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 S1[ set , set ] means ex x9 being Subset of L st
( x9 = \$1 & \$2 = sup x9 );
take Y = ATOM L; :: thesis:
A3: for x being Element of () ex y being Element of L st S1[x,y]
proof
let x be Element of (); :: thesis: ex y being Element of L st S1[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: S1[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 (),L such that
A4: for x being Element of () holds S1[x,f . x] from
A5: now :: thesis: for z, v being Element of () holds
( ( z <= v implies f . z <= f . v ) & ( f . z <= f . v implies z <= v ) )
let z, v be Element of (); :: 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 ;
thus ( z <= v implies f . z <= f . v ) by ; :: thesis: ( f . z <= f . v implies z <= v )
A11: v9 c= ATOM L by ;
A12: z9 c= ATOM L by ;
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 () by ;
then K in the carrier of () ;
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 ;
hence k in rng f by ; :: thesis: verum
end;
then A17: rng f = the carrier of L by XBOOLE_0:def 10;
now :: thesis: for z, v being Element of () st f . z = f . v holds
z = v
let z, v be Element of (); :: 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 ;
z9 c= ATOM L by ;
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 V13() ;
then f is isomorphic by ;
then BoolePoset Y,L are_isomorphic ;
hence L, BoolePoset Y are_isomorphic by WAYBEL_1:6; :: thesis: verum