let L be non empty transitive antisymmetric with_infima RelStr ; :: thesis: for x being Element of
for X, Y being Subset of st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of : y in X } holds
x "/\" (sup X) >= sup Y
let x be Element of ; :: thesis: for X, Y being Subset of st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of : y in X } holds
x "/\" (sup X) >= sup Y
let X, Y be Subset of ; :: thesis: ( ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of : y in X } implies x "/\" (sup X) >= sup Y )
assume that
A1: ex_sup_of X,L and
A2: ex_sup_of Y,L and
A3: Y = { (x "/\" y) where y is Element of : y in X } ; :: thesis: x "/\" (sup X) >= sup Y
Y is_<=_than x "/\" (sup X)

proof

let y be Element of ; :: according to LATTICE3:def 9 :: thesis: ( not y in Y or y <= x "/\" (sup X) )
assume y in Y ; :: thesis: y <= x "/\" (sup X)
then consider z being Element of such that
A4: y = x "/\" z and
A5: z in X by A3;
A6: y <= z by A4, YELLOW_0:23;
X is_<=_than sup X by A1, YELLOW_0:30;
then z <= sup X by A5, LATTICE3:def 9;
then A7: y <= sup X by A6, YELLOW_0:def 2;
y <= x by A4, YELLOW_0:23;
hence y <= x "/\" (sup X) by A7, YELLOW_0:23; :: thesis: verum

end;

hence x "/\" (sup X) >= sup Y by A2, YELLOW_0:30; :: thesis: verum