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

set R = LattRel L1;
set S = LattRel L2;
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;
A2: dom F = field (LattRel L1) by A1, WELLORD1:def 7;
A3: ( field (LattRel L2) = the carrier of L2 & rng F = field (LattRel L2) ) by A1, FILTER_1:32, WELLORD1:def 7;
A4: field (LattRel L1) = the carrier of L1 by FILTER_1:32;
then reconsider F = F as Function of L1,L2 by A2, A3, FUNCT_2:1;

now :: thesis: for a1, b1 being Element of L1 holds
( F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) & F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) )

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

proof

b19 [= a19 "\/" b19 by LATTICES:5;
then [b1,(a1 "\/" b1)] in LattRel L1 by FILTER_1:31;
then [(F . b1),(F . (a1 "\/" b1))] in LattRel L2 by A1, WELLORD1:def 7;
then A6: F . b19 [= F . (a19 "\/" b19) by FILTER_1:31;
consider k1 being Element of L1 such that
A7: (F . a1) "\/" (F . b1) = F . k1 by A5, Th6;
F . b1 [= F . k1 by A7, LATTICES:5;
then [(F . b1),(F . k1)] in LattRel L2 by FILTER_1:31;
then [b1,k1] in LattRel L1 by A1, A4, WELLORD1:def 7;
then A8: b1 [= k1 by FILTER_1:31;
F . a1 [= F . k1 by A7, LATTICES:5;
then [(F . a1),(F . k1)] in LattRel L2 by FILTER_1:31;
then [a1,k1] in LattRel L1 by A1, A4, WELLORD1:def 7;
then a1 [= k1 by FILTER_1:31;
then a1 "\/" b1 [= k1 by A8, FILTER_0:6;
then [(a1 "\/" b1),k1] in LattRel L1 by FILTER_1:31;
then [(F . (a1 "\/" b1)),(F . k1)] in LattRel L2 by A1, WELLORD1:def 7;
then A9: F . (a1 "\/" b1) [= (F . a1) "\/" (F . b1) by A7, FILTER_1:31;
a19 [= a19 "\/" b19 by LATTICES:5;
then [a1,(a1 "\/" b1)] in LattRel L1 by FILTER_1:31;
then [(F . a1),(F . (a1 "\/" b1))] in LattRel L2 by A1, WELLORD1:def 7;
then F . a19 [= F . (a19 "\/" b19) by FILTER_1:31;
then (F . a1) "\/" (F . b1) [= F . (a1 "\/" b1) by A6, FILTER_0:6;
hence F . (a1 "\/" b1) = (F . a1) "\/" (F . b1) by A9, LATTICES:8; :: thesis: verum

end;

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

proof

a19 "/\" b19 [= b19 by LATTICES:6;
then [(a1 "/\" b1),b1] in LattRel L1 by FILTER_1:31;
then [(F . (a1 "/\" b1)),(F . b1)] in LattRel L2 by A1, WELLORD1:def 7;
then A10: F . (a19 "/\" b19) [= F . b19 by FILTER_1:31;
consider k1 being Element of L1 such that
A11: (F . a1) "/\" (F . b1) = F . k1 by A5, Th6;
F . k1 [= F . b1 by A11, LATTICES:6;
then [(F . k1),(F . b1)] in LattRel L2 by FILTER_1:31;
then [k1,b1] in LattRel L1 by A1, A4, WELLORD1:def 7;
then A12: k1 [= b1 by FILTER_1:31;
F . k1 [= F . a1 by A11, LATTICES:6;
then [(F . k1),(F . a1)] in LattRel L2 by FILTER_1:31;
then [k1,a1] in LattRel L1 by A1, A4, WELLORD1:def 7;
then k1 [= a1 by FILTER_1:31;
then k1 [= a1 "/\" b1 by A12, FILTER_0:7;
then [k1,(a1 "/\" b1)] in LattRel L1 by FILTER_1:31;
then [(F . k1),(F . (a1 "/\" b1))] in LattRel L2 by A1, WELLORD1:def 7;
then A13: (F . a1) "/\" (F . b1) [= F . (a1 "/\" b1) by A11, FILTER_1:31;
a19 "/\" b19 [= a19 by LATTICES:6;
then [(a1 "/\" b1),a1] in LattRel L1 by FILTER_1:31;
then [(F . (a1 "/\" b1)),(F . a1)] in LattRel L2 by A1, WELLORD1:def 7;
then F . (a19 "/\" b19) [= F . a19 by FILTER_1:31;
then F . (a1 "/\" b1) [= (F . a1) "/\" (F . b1) by A10, FILTER_0:7;
hence F . (a1 "/\" b1) = (F . a1) "/\" (F . b1) by A13, LATTICES:8; :: thesis: verum

end;

end;

then ( F is "\/"-preserving & F is "/\"-preserving ) ;
then reconsider F = F as Homomorphism of L1,L2 ;
take F ; :: thesis: F is bijective
( F is one-to-one & F is onto ) by A1, A3, FUNCT_2:def 3, WELLORD1:def 7;
hence F is bijective ; :: thesis: verum

end;

set R = LattRel L1;
set S = LattRel L2;
given f being Homomorphism of L1,L2 such that A14: f is bijective ; :: thesis: L1,L2 are_isomorphic
A15: for a, b being object 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 object ; :: 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:15; :: thesis: [(f . a),(f . b)] in LattRel L2
then reconsider a9 = a, b9 = b as Element of L1 by FILTER_1:32;
a9 [= b9 by A16, FILTER_1:31;
then f . a9 [= f . b9 by A14, Th5;
hence [(f . a),(f . b)] in LattRel L2 by FILTER_1:31; :: thesis: verum

end;

assume that
A17: ( a in field (LattRel L1) & b in field (LattRel L1) ) and
A18: [(f . a),(f . b)] in LattRel L2 ; :: thesis: [a,b] in LattRel L1
reconsider a9 = a, b9 = b as Element of L1 by A17, FILTER_1:32;
f . a9 [= f . b9 by A18, FILTER_1:31;
then a9 [= b9 by A14, Th5;
hence [a,b] in LattRel L1 by FILTER_1:31; :: thesis: verum

end;

A19: dom f = the carrier of L1 by FUNCT_2:def 1
.= field (LattRel L1) by FILTER_1:32 ;
rng f = the carrier of L2 by A14, FUNCT_2:def 3
.= field (LattRel L2) by FILTER_1:32 ;
then f is_isomorphism_of LattRel L1, LattRel L2 by A14, A19, 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