let L, M be complete continuous LATTICE; :: thesis: for F, G being set st F is_FreeGen_set_of L & G is_FreeGen_set_of M & card F = card G holds

L,M are_isomorphic

let Lg, Mg be set ; :: thesis: ( Lg is_FreeGen_set_of L & Mg is_FreeGen_set_of M & card Lg = card Mg implies L,M are_isomorphic )

assume that

A1: Lg is_FreeGen_set_of L and

A2: Mg is_FreeGen_set_of M and

A3: card Lg = card Mg ; :: thesis: L,M are_isomorphic

Lg,Mg are_equipotent by A3, CARD_1:5;

then consider f being Function such that

A4: f is one-to-one and

A5: dom f = Lg and

A6: rng f = Mg ;

set g = f " ;

A7: dom (f ") = Mg by A4, A6, FUNCT_1:33;

reconsider Mg = Mg as Subset of M by A2, Th7;

A8: rng (f ") = Lg by A4, A5, FUNCT_1:33;

reconsider Lg = Lg as Subset of L by A1, Th7;

Mg c= the carrier of M ;

then reconsider f = f as Function of Lg, the carrier of M by A5, A6, FUNCT_2:def 1, RELSET_1:4;

consider F being CLHomomorphism of L,M such that

A9: F | Lg = f and

for h9 being CLHomomorphism of L,M st h9 | Lg = f holds

h9 = F by A1;

Lg c= the carrier of L ;

then reconsider g = f " as Function of Mg, the carrier of L by A7, A8, FUNCT_2:def 1, RELSET_1:4;

consider G being CLHomomorphism of M,L such that

A10: G | Mg = g and

for h9 being CLHomomorphism of M,L st h9 | Mg = g holds

h9 = G by A2;

reconsider GF = G * F as CLHomomorphism of L,L by Th2;

GF | Lg = G * f by A9, RELAT_1:83

.= g * f by A6, A10, FUNCT_4:2

.= id Lg by A4, A5, FUNCT_1:39 ;

then A11: GF = id L by A1, Th8;

then A12: F is V13() by FUNCT_2:23;

reconsider FG = F * G as CLHomomorphism of M,M by Th2;

F is directed-sups-preserving by WAYBEL16:def 1;

then A13: F is monotone by WAYBEL17:3;

G is directed-sups-preserving by WAYBEL16:def 1;

then A14: G is monotone by WAYBEL17:3;

FG | Mg = F * g by A10, RELAT_1:83

.= f * g by A8, A9, FUNCT_4:2

.= id Mg by A4, A6, FUNCT_1:39 ;

then FG = id M by A2, Th8;

then F is onto by FUNCT_2:23;

then rng F = the carrier of M by FUNCT_2:def 3;

then G = F " by A11, A12, FUNCT_2:30;

then F is isomorphic by A12, A13, A14, WAYBEL_0:def 38;

hence L,M are_isomorphic by WAYBEL_1:def 8; :: thesis: verum

L,M are_isomorphic

let Lg, Mg be set ; :: thesis: ( Lg is_FreeGen_set_of L & Mg is_FreeGen_set_of M & card Lg = card Mg implies L,M are_isomorphic )

assume that

A1: Lg is_FreeGen_set_of L and

A2: Mg is_FreeGen_set_of M and

A3: card Lg = card Mg ; :: thesis: L,M are_isomorphic

Lg,Mg are_equipotent by A3, CARD_1:5;

then consider f being Function such that

A4: f is one-to-one and

A5: dom f = Lg and

A6: rng f = Mg ;

set g = f " ;

A7: dom (f ") = Mg by A4, A6, FUNCT_1:33;

reconsider Mg = Mg as Subset of M by A2, Th7;

A8: rng (f ") = Lg by A4, A5, FUNCT_1:33;

reconsider Lg = Lg as Subset of L by A1, Th7;

Mg c= the carrier of M ;

then reconsider f = f as Function of Lg, the carrier of M by A5, A6, FUNCT_2:def 1, RELSET_1:4;

consider F being CLHomomorphism of L,M such that

A9: F | Lg = f and

for h9 being CLHomomorphism of L,M st h9 | Lg = f holds

h9 = F by A1;

Lg c= the carrier of L ;

then reconsider g = f " as Function of Mg, the carrier of L by A7, A8, FUNCT_2:def 1, RELSET_1:4;

consider G being CLHomomorphism of M,L such that

A10: G | Mg = g and

for h9 being CLHomomorphism of M,L st h9 | Mg = g holds

h9 = G by A2;

reconsider GF = G * F as CLHomomorphism of L,L by Th2;

GF | Lg = G * f by A9, RELAT_1:83

.= g * f by A6, A10, FUNCT_4:2

.= id Lg by A4, A5, FUNCT_1:39 ;

then A11: GF = id L by A1, Th8;

then A12: F is V13() by FUNCT_2:23;

reconsider FG = F * G as CLHomomorphism of M,M by Th2;

F is directed-sups-preserving by WAYBEL16:def 1;

then A13: F is monotone by WAYBEL17:3;

G is directed-sups-preserving by WAYBEL16:def 1;

then A14: G is monotone by WAYBEL17:3;

FG | Mg = F * g by A10, RELAT_1:83

.= f * g by A8, A9, FUNCT_4:2

.= id Mg by A4, A6, FUNCT_1:39 ;

then FG = id M by A2, Th8;

then F is onto by FUNCT_2:23;

then rng F = the carrier of M by FUNCT_2:def 3;

then G = F " by A11, A12, FUNCT_2:30;

then F is isomorphic by A12, A13, A14, WAYBEL_0:def 38;

hence L,M are_isomorphic by WAYBEL_1:def 8; :: thesis: verum