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 )

( 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

thus
( sup X <= sup Y implies X c= Y )
:: thesis: verum
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;assume X c= Y ; :: thesis: sup X <= sup Y

hence sup X <= sup Y by A3, YELLOW_0:34; :: thesis: verum

proof

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

thus X c= Y :: thesis: verum

end;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;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