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 )

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 ) )

.= 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

proof

set R = LattRel L1;
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;

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 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) )

then
( F is "\/"-preserving & F is "/\"-preserving )
;( 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)

end;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

thus
F . (a1 "/\" b1) = (F . a1) "/\" (F . b1)
:: thesis: verum
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;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

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;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

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

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

A19: dom f =
the carrier of L1
by FUNCT_2:def 1
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 ) )

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;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 that 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;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

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

.= 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