let L be complete Boolean LATTICE; :: thesis: for X, Y being Subset of L st X c= ATOM L & Y c= ATOM L holds
( X c= Y iff sup X <= sup Y )
let X, Y be Subset of L; :: thesis: ( X c= ATOM L & Y c= ATOM L implies ( X c= Y iff sup X <= sup Y ) )
assume that
A1: X c= ATOM L and
A2: Y c= ATOM L ; :: thesis: ( X c= Y iff sup X <= sup Y )
thus ( X c= Y implies sup X <= sup Y ) :: thesis: ( sup X <= sup Y implies X c= Y )

proof

A3: ( ex_sup_of X,L & ex_sup_of Y,L ) by YELLOW_0:17;
assume X c= Y ; :: thesis: sup X <= sup Y
hence sup X <= sup Y by A3, YELLOW_0:34; :: thesis: verum

end;

thus ( sup X <= sup Y implies X c= Y ) :: thesis: verum

proof

assume A4: sup X <= sup Y ; :: thesis: X c= Y
thus X c= Y :: thesis: verum

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X or z in Y )
assume A5: z in X ; :: thesis: z in Y
then reconsider z1 = z as Element of L ;
sup X is_>=_than X by YELLOW_0:32;
then z1 <= sup X by A5, LATTICE3:def 9;
then A6: z1 <= sup Y by A4, ORDERS_2:3;
z1 is atom by A1, A5, Def2;
hence z in Y by A2, A6, Th25; :: thesis: verum

end;

end;