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
take Y = ATOM L; :: thesis: L, BoolePoset Y are_isomorphic
defpred S₁[ set , set ] means ex x' being Subset of L st
( x' = $1 & $2 = sup x' );
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:28;
then reconsider x' = x as Subset of L 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 (BoolePoset Y) holds S₁[x,f . x] from FUNCT_2:sch 10(A3);

now

let z, v be Element of (BoolePoset Y); :: thesis: ( f . z = f . v implies z = v )
consider z' being Subset of L such that
A5: z' = z and
A6: f . z = sup z' by A4;
consider v' being Subset of L such that
A7: v' = v and
A8: f . v = sup v' by A4;
A9: z' c= ATOM L by A5, WAYBEL_8:28;
A10: v' c= ATOM L by A7, WAYBEL_8:28;
assume f . z = f . v ; :: thesis: z = v
then ( z c= v & v c= z ) by A1, A5, A6, A7, A8, A9, A10, Th29;
hence z = v by XBOOLE_0:def 10; :: thesis: verum

end;

then A11: f is one-to-one by WAYBEL_1:def 1;
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 L such that
A12: K c= ATOM L and
A13: k = sup K by A2;
A14: K is Element of (BoolePoset Y) by A12, WAYBEL_8:28;
then ( K in the carrier of (BoolePoset Y) & not the carrier of L is empty ) ;
then A15: K in dom f by FUNCT_2:def 1;
consider K' being Subset of L such that
A16: K' = K and
A17: f . K = sup K' by A4, A14;
thus k in rng f by A13, A15, A16, A17, FUNCT_1:def 5; :: thesis: verum

end;

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

now

let z, v be Element of (BoolePoset Y); :: thesis: ( ( z <= v implies f . z <= f . v ) & ( f . z <= f . v implies z <= v ) )
consider z' being Subset of L such that
A19: z' = z and
A20: f . z = sup z' by A4;
consider v' being Subset of L such that
A21: v' = v and
A22: f . v = sup v' by A4;
A23: ex_sup_of z',L by A1, YELLOW_0:17;
A24: ex_sup_of v',L by A1, YELLOW_0:17;
A25: z' c= ATOM L by A19, WAYBEL_8:28;
A26: v' c= ATOM L by A21, WAYBEL_8:28;
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 A19, A20, A21, A22, A23, A24, YELLOW_0:34; :: thesis: verum

end;

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, A19, A20, A21, A22, A25, A26, Th29;
hence z <= v by YELLOW_1:2; :: thesis: verum

end;

end;

then f is isomorphic by A11, A18, 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