let L be Boolean LATTICE; :: thesis: ( L is complete & ( for x being Element of ex X being Subset of 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 ex X being Subset of 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 x' being Subset of st
( x' = $1 & $2 = sup x' );
take Y = ATOM L; :: thesis: L, BoolePoset Y are_isomorphic
A3: for x being Element of ex y being Element of st S₁[x,y]

proof

let x be Element of ; :: thesis: ex y being Element of st S₁[x,y]
x c= Y by WAYBEL_8:28;
then reconsider x' = x as Subset of by XBOOLE_1:1;
take y = sup x'; :: thesis: S₁[x,y]
take x' ; :: thesis: ( x' = x & y = sup x' )
thus ( x' = x & y = sup x' ) ; :: thesis: verum

end;

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

A5: now

let z, v be Element of ; :: thesis: ( ( z <= v implies f . z <= f . v ) & ( f . z <= f . v implies z <= v ) )
consider z' being Subset of such that
A6: z' = z and
A7: f . z = sup z' by A4;
consider v' being Subset of such that
A8: v' = v and
A9: f . v = sup v' by A4;
A10: ( ex_sup_of z',L & ex_sup_of v',L ) by A1, YELLOW_0:17;
thus ( z <= v implies f . z <= f . v ) :: thesis: ( f . z <= f . v implies z <= v )

proof

assume z <= v ; :: thesis: f . z <= f . v
then z c= v by YELLOW_1:2;
hence f . z <= f . v by A6, A7, A8, A9, A10, YELLOW_0:34; :: thesis: verum

end;

A11: v' c= ATOM L by A8, WAYBEL_8:28;
A12: z' c= ATOM L by A6, WAYBEL_8:28;
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, Th29;
hence z <= v by YELLOW_1:2; :: thesis: verum

end;

end;

the carrier of L c= rng f

proof

let k be set ; :: 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 such that
A13: K c= ATOM L and
A14: k = sup K by A2;
A15: K is Element of by A13, WAYBEL_8:28;
then K in the carrier of (BoolePoset Y) ;
then A16: K in dom f by FUNCT_2:def 1;
ex K' being Subset of st
( K' = K & f . K = sup K' ) by A4, A15;
hence k in rng f by A14, A16, FUNCT_1:def 5; :: thesis: verum

end;

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

now

let z, v be Element of ; :: thesis: ( f . z = f . v implies z = v )
assume A18: f . z = f . v ; :: thesis: z = v
consider z' being Subset of such that
A19: z' = z and
A20: f . z = sup z' by A4;
consider v' being Subset of such that
A21: v' = v and
A22: f . v = sup v' by A4;
A23: v' c= ATOM L by A21, WAYBEL_8:28;
z' c= ATOM L by A19, WAYBEL_8:28;
then ( z c= v & v c= z ) by A1, A19, A20, A21, A22, A23, A18, Th29;
hence z = v by XBOOLE_0:def 10; :: thesis: verum

end;

then f is one-to-one by WAYBEL_1:def 1;
then f is isomorphic by A17, A5, WAYBEL_0:66;
then BoolePoset Y,L are_isomorphic by WAYBEL_1:def 8;
hence L, BoolePoset Y are_isomorphic by WAYBEL_1:7; :: thesis: verum