let L be Boolean LATTICE; :: thesis: ( L is complete & ( for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ) implies ex Y being set st L, BoolePoset Y are_isomorphic )

assume that

A1: L is complete and

A2: for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ; :: thesis: ex Y being set st L, BoolePoset Y are_isomorphic

defpred S_{1}[ set , set ] means ex x9 being Subset of L st

( x9 = $1 & $2 = sup x9 );

take Y = ATOM L; :: thesis: L, BoolePoset Y are_isomorphic

A3: for x being Element of (BoolePoset Y) ex y being Element of L st S_{1}[x,y]

A4: for x being Element of (BoolePoset Y) holds S_{1}[x,f . x]
from FUNCT_2:sch 3(A3);

then f is isomorphic by A17, A5, WAYBEL_0:66;

then BoolePoset Y,L are_isomorphic ;

hence L, BoolePoset Y are_isomorphic by WAYBEL_1:6; :: thesis: verum

( X c= ATOM L & x = sup X ) ) implies ex Y being set st L, BoolePoset Y are_isomorphic )

assume that

A1: L is complete and

A2: for x being Element of L ex X being Subset of L st

( X c= ATOM L & x = sup X ) ; :: thesis: ex Y being set st L, BoolePoset Y are_isomorphic

defpred S

( x9 = $1 & $2 = sup x9 );

take Y = ATOM L; :: thesis: L, BoolePoset Y are_isomorphic

A3: for x being Element of (BoolePoset Y) ex y being Element of L st S

proof

consider f being Function of (BoolePoset Y),L such that
let x be Element of (BoolePoset Y); :: thesis: ex y being Element of L st S_{1}[x,y]

x c= Y by WAYBEL_8:26;

then reconsider x9 = x as Subset of L by XBOOLE_1:1;

take sup x9 ; :: thesis: S_{1}[x, sup x9]

take x9 ; :: thesis: ( x9 = x & sup x9 = sup x9 )

thus ( x9 = x & sup x9 = sup x9 ) ; :: thesis: verum

end;x c= Y by WAYBEL_8:26;

then reconsider x9 = x as Subset of L by XBOOLE_1:1;

take sup x9 ; :: thesis: S

take x9 ; :: thesis: ( x9 = x & sup x9 = sup x9 )

thus ( x9 = x & sup x9 = sup x9 ) ; :: thesis: verum

A4: for x being Element of (BoolePoset Y) holds S

A5: now :: thesis: for z, v being Element of (BoolePoset Y) holds

( ( z <= v implies f . z <= f . v ) & ( f . z <= f . v implies z <= v ) )

the carrier of L c= rng f
( ( z <= v implies f . z <= f . v ) & ( f . z <= f . v implies z <= v ) )

let z, v be Element of (BoolePoset Y); :: thesis: ( ( z <= v implies f . z <= f . v ) & ( f . z <= f . v implies z <= v ) )

consider z9 being Subset of L such that

A6: z9 = z and

A7: f . z = sup z9 by A4;

consider v9 being Subset of L such that

A8: v9 = v and

A9: f . v = sup v9 by A4;

A10: ( ex_sup_of z9,L & ex_sup_of v9,L ) by A1, YELLOW_0:17;

thus ( z <= v implies f . z <= f . v ) by YELLOW_1:2, A6, A7, A8, A9, A10, YELLOW_0:34; :: thesis: ( f . z <= f . v implies z <= v )

A11: v9 c= ATOM L by A8, WAYBEL_8:26;

A12: z9 c= ATOM L by A6, WAYBEL_8:26;

thus ( f . z <= f . v implies z <= v ) :: thesis: verum

end;consider z9 being Subset of L such that

A6: z9 = z and

A7: f . z = sup z9 by A4;

consider v9 being Subset of L such that

A8: v9 = v and

A9: f . v = sup v9 by A4;

A10: ( ex_sup_of z9,L & ex_sup_of v9,L ) by A1, YELLOW_0:17;

thus ( z <= v implies f . z <= f . v ) by YELLOW_1:2, A6, A7, A8, A9, A10, YELLOW_0:34; :: thesis: ( f . z <= f . v implies z <= v )

A11: v9 c= ATOM L by A8, WAYBEL_8:26;

A12: z9 c= ATOM L by A6, WAYBEL_8:26;

thus ( f . z <= f . v implies z <= v ) :: thesis: verum

proof

then A17:
rng f = the carrier of L
by XBOOLE_0:def 10;
let k be object ; :: according to TARSKI:def 3 :: thesis: ( not k in the carrier of L or k in rng f )

assume k in the carrier of L ; :: thesis: k in rng f

then consider K being Subset of L such that

A13: K c= ATOM L and

A14: k = sup K by A2;

A15: K is Element of (BoolePoset Y) by A13, WAYBEL_8:26;

then K in the carrier of (BoolePoset Y) ;

then A16: K in dom f by FUNCT_2:def 1;

ex K9 being Subset of L st

( K9 = K & f . K = sup K9 ) by A4, A15;

hence k in rng f by A14, A16, FUNCT_1:def 3; :: thesis: verum

end;assume k in the carrier of L ; :: thesis: k in rng f

then consider K being Subset of L such that

A13: K c= ATOM L and

A14: k = sup K by A2;

A15: K is Element of (BoolePoset Y) by A13, WAYBEL_8:26;

then K in the carrier of (BoolePoset Y) ;

then A16: K in dom f by FUNCT_2:def 1;

ex K9 being Subset of L st

( K9 = K & f . K = sup K9 ) by A4, A15;

hence k in rng f by A14, A16, FUNCT_1:def 3; :: thesis: verum

now :: thesis: for z, v being Element of (BoolePoset Y) st f . z = f . v holds

z = v

then
f is V13()
;z = v

let z, v be Element of (BoolePoset Y); :: thesis: ( f . z = f . v implies z = v )

assume A18: f . z = f . v ; :: thesis: z = v

consider z9 being Subset of L such that

A19: z9 = z and

A20: f . z = sup z9 by A4;

consider v9 being Subset of L such that

A21: v9 = v and

A22: f . v = sup v9 by A4;

A23: v9 c= ATOM L by A21, WAYBEL_8:26;

z9 c= ATOM L by A19, WAYBEL_8:26;

then ( z c= v & v c= z ) by A1, A19, A20, A21, A22, A23, A18, Th26;

hence z = v by XBOOLE_0:def 10; :: thesis: verum

end;assume A18: f . z = f . v ; :: thesis: z = v

consider z9 being Subset of L such that

A19: z9 = z and

A20: f . z = sup z9 by A4;

consider v9 being Subset of L such that

A21: v9 = v and

A22: f . v = sup v9 by A4;

A23: v9 c= ATOM L by A21, WAYBEL_8:26;

z9 c= ATOM L by A19, WAYBEL_8:26;

then ( z c= v & v c= z ) by A1, A19, A20, A21, A22, A23, A18, Th26;

hence z = v by XBOOLE_0:def 10; :: thesis: verum

then f is isomorphic by A17, A5, WAYBEL_0:66;

then BoolePoset Y,L are_isomorphic ;

hence L, BoolePoset Y are_isomorphic by WAYBEL_1:6; :: thesis: verum