let L1, L2 be non empty RelStr ; :: thesis: ( RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) implies L1,L2 are_isomorphic )
assume A1: RelStr(# the carrier of L1, the InternalRel of L1 #) = RelStr(# the carrier of L2, the InternalRel of L2 #) ; :: thesis: L1,L2 are_isomorphic
ex f being Function of L1,L2 st f is isomorphic
proof
reconsider f = id the carrier of L1 as Function of L1,L2 by A1;
take f ; :: thesis: f is isomorphic
now :: thesis: for z being object st z in the carrier of L2 holds
ex v being object st
( v in the carrier of L1 & z = f . v )
let z be object ; :: thesis: ( z in the carrier of L2 implies ex v being object st
( v in the carrier of L1 & z = f . v ) )
assume A2: z in the carrier of L2 ; :: thesis: ex v being object st
( v in the carrier of L1 & z = f . v )
take v = z; :: thesis: ( v in the carrier of L1 & z = f . v )
thus v in the carrier of L1 by A1, A2; :: thesis: z = f . v
thus z = f . v by A1, A2, FUNCT_1:18; :: thesis: verum
end;
then A3: rng f = the carrier of L2 by FUNCT_2:10;
for x, y being Element of L1 holds
( x <= y iff f . x <= f . y ) by A1, YELLOW_0:1;
hence f is isomorphic by A3, WAYBEL_0:66; :: thesis: verum
end;
hence L1,L2 are_isomorphic by WAYBEL_1:def 8; :: thesis: verum