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₁[ 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₁[x,y]

proof

let x be Element of (BoolePoset Y); :: thesis: ex y being Element of L st S₁[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₁[x, sup x9]
take x9 ; :: thesis: ( x9 = x & sup x9 = sup x9 )
thus ( x9 = x & sup x9 = sup x9 ) ; :: thesis: verum

end;

consider f being Function of (BoolePoset Y),L such that
A4: for x being Element of (BoolePoset Y) holds S₁[x,f . x] from FUNCT_2:sch 3(A3);

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

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

proof

assume f . z <= f . v ; :: thesis: z <= v
then z c= v by A1, A6, A7, A8, A9, A12, A11, Th26;
hence z <= v by YELLOW_1:2; :: thesis: verum

end;

end;

the carrier of L c= rng f

proof

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;

then A17: rng f = the carrier of L by XBOOLE_0:def 10;

now :: thesis: for z, v being Element of (BoolePoset Y) st f . z = f . v holds
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;

then f is one-to-one ;
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