thus ( L1,L2 are_isomorphic implies ex f being Homomorphism of L1,L2 st f is bijective ) :: thesis: ( ex f being Homomorphism of L1,L2 st f is bijective implies L1,L2 are_isomorphic )

proof

assume L1,L2 are_isomorphic ; :: thesis: ex f being Homomorphism of L1,L2 st f is bijective
then LattRel L1, LattRel L2 are_isomorphic by FILTER_1:def 9;
then consider F being Function such that
A1: F is_isomorphism_of LattRel L1, LattRel L2 by WELLORD1:def 8;
set R = LattRel L1;
set S = LattRel L2;
A2: ( field (LattRel L2) = the carrier of L2 & field (LattRel L1) = the carrier of L1 ) by FILTER_1:33;
A3: ( dom F = field (LattRel L1) & rng F = field (LattRel L2) & F is one-to-one & ( for a, b being set holds
( [a,b] in LattRel L1 iff ( a in field (LattRel L1) & b in field (LattRel L1) & [(F . a),(F . b)] in LattRel L2 ) ) ) ) by A1, WELLORD1:def 7;
then reconsider F = F as Function of the carrier of L1,the carrier of L2 by A2, FUNCT_2:3;

now

let a1, b1 be Element of L1; :: thesis: ( F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) & F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) )
reconsider a1' = a1, b1' = b1 as Element of L1 ;
A4: F is onto by A2, A3, FUNCT_2:def 3;
thus F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) :: thesis: F . (a1 "/\" b1) = (F . a1) "/\" (F . b1)

proof

consider k1 being Element of L1 such that
A5: (F . a1) "\/" (F . b1) = F . k1 by A4, Th9;
( F . a1 [= F . k1 & F . b1 [= F . k1 ) by A5, LATTICES:22;
then ( [(F . a1),(F . k1)] in LattRel L2 & [(F . b1),(F . k1)] in LattRel L2 ) by FILTER_1:32;
then ( [a1,k1] in LattRel L1 & [b1,k1] in LattRel L1 ) by A1, A2, WELLORD1:def 7;
then ( a1 [= k1 & b1 [= k1 ) by FILTER_1:32;
then a1 "\/" b1 [= k1 by FILTER_0:6;
then [(a1 "\/" b1),k1] in LattRel L1 by FILTER_1:32;
then [(F . (a1 "\/" b1)),(F . k1)] in LattRel L2 by A1, WELLORD1:def 7;
then A6: F . (a1 "\/" b1) [= (F . a1) "\/" (F . b1) by A5, FILTER_1:32;
a1' [= a1' "\/" b1' by LATTICES:22;
then [a1,(a1 "\/" b1)] in LattRel L1 by FILTER_1:32;
then [(F . a1),(F . (a1 "\/" b1))] in LattRel L2 by A1, WELLORD1:def 7;
then A7: F . a1' [= F . (a1' "\/" b1') by FILTER_1:32;
b1' [= a1' "\/" b1' by LATTICES:22;
then [b1,(a1 "\/" b1)] in LattRel L1 by FILTER_1:32;
then [(F . b1),(F . (a1 "\/" b1))] in LattRel L2 by A1, WELLORD1:def 7;
then F . b1' [= F . (a1' "\/" b1') by FILTER_1:32;
then (F . a1) "\/" (F . b1) [= F . (a1 "\/" b1) by A7, FILTER_0:6;
hence F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) by A6, LATTICES:26; :: thesis: verum

end;

thus F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) :: thesis: verum

proof

consider k1 being Element of L1 such that
A8: (F . a1) "/\" (F . b1) = F . k1 by A4, Th9;
( F . k1 [= F . a1 & F . k1 [= F . b1 ) by A8, LATTICES:23;
then ( [(F . k1),(F . a1)] in LattRel L2 & [(F . k1),(F . b1)] in LattRel L2 ) by FILTER_1:32;
then ( [k1,a1] in LattRel L1 & [k1,b1] in LattRel L1 ) by A1, A2, WELLORD1:def 7;
then ( k1 [= a1 & k1 [= b1 ) by FILTER_1:32;
then k1 [= a1 "/\" b1 by FILTER_0:7;
then [k1,(a1 "/\" b1)] in LattRel L1 by FILTER_1:32;
then [(F . k1),(F . (a1 "/\" b1))] in LattRel L2 by A1, WELLORD1:def 7;
then A9: (F . a1) "/\" (F . b1) [= F . (a1 "/\" b1) by A8, FILTER_1:32;
a1' "/\" b1' [= a1' by LATTICES:23;
then [(a1 "/\" b1),a1] in LattRel L1 by FILTER_1:32;
then [(F . (a1 "/\" b1)),(F . a1)] in LattRel L2 by A1, WELLORD1:def 7;
then A10: F . (a1' "/\" b1') [= F . a1' by FILTER_1:32;
a1' "/\" b1' [= b1' by LATTICES:23;
then [(a1 "/\" b1),b1] in LattRel L1 by FILTER_1:32;
then [(F . (a1 "/\" b1)),(F . b1)] in LattRel L2 by A1, WELLORD1:def 7;
then F . (a1' "/\" b1') [= F . b1' by FILTER_1:32;
then F . (a1 "/\" b1) [= (F . a1) "/\" (F . b1) by A10, FILTER_0:7;
hence F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) by A9, LATTICES:26; :: thesis: verum

end;

end;

then reconsider F = F as Homomorphism of L1,L2 by Def1;
take F ; :: thesis: F is bijective
( F is one-to-one & F is onto ) by A2, A3, FUNCT_2:def 3;
hence F is bijective ; :: thesis: verum

end;

given f being Homomorphism of L1,L2 such that A11: f is bijective ; :: thesis: L1,L2 are_isomorphic
A12: ( f is one-to-one & f is onto ) by A11;
then A13: f is one-to-one ;
set R = LattRel L1;
set S = LattRel L2;
A14: dom f = the carrier of L1 by FUNCT_2:def 1
.= field (LattRel L1) by FILTER_1:33 ;
A15: rng f = the carrier of L2 by A12, FUNCT_2:def 3
.= field (LattRel L2) by FILTER_1:33 ;
for a, b being set holds
( [a,b] in LattRel L1 iff ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 ) )

proof

let a, b be set ; :: thesis: ( [a,b] in LattRel L1 iff ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 ) )

hereby :: thesis: ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 implies [a,b] in LattRel L1 )

assume A16: [a,b] in LattRel L1 ; :: thesis: ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 )
hence ( a in field (LattRel L1) & b in field (LattRel L1) ) by RELAT_1:30; :: thesis: [(f . a),(f . b)] in LattRel L2
then reconsider a' = a, b' = b as Element of L1 by FILTER_1:33;
a' [= b' by A16, FILTER_1:32;
then f . a' [= f . b' by A12, Th8;
hence [(f . a),(f . b)] in LattRel L2 by FILTER_1:32; :: thesis: verum

end;

assume A17: ( a in field (LattRel L1) & b in field (LattRel L1) & [(f . a),(f . b)] in LattRel L2 ) ; :: thesis: [a,b] in LattRel L1
then reconsider a' = a, b' = b as Element of L1 by FILTER_1:33;
f . a' [= f . b' by A17, FILTER_1:32;
then a' [= b' by A12, Th8;
hence [a,b] in LattRel L1 by FILTER_1:32; :: thesis: verum

end;

then f is_isomorphism_of LattRel L1, LattRel L2 by A13, A14, A15, WELLORD1:def 7;
then LattRel L1, LattRel L2 are_isomorphic by WELLORD1:def 8;
hence L1,L2 are_isomorphic by FILTER_1:def 9; :: thesis: verum