let L be non empty transitive antisymmetric with_infima RelStr ; :: thesis: for x being Element of L
for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } holds
x "/\" (sup X) >= sup Y
let x be Element of L; :: thesis: for X, Y being Subset of L st ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : y in X } holds
x "/\" (sup X) >= sup Y
let X, Y be Subset of L; :: thesis: ( ex_sup_of X,L & ex_sup_of Y,L & Y = { (x "/\" y) where y is Element of L : 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 L : y in X } ; :: thesis: x "/\" (sup X) >= sup Y
Y is_<=_than x "/\" (sup X)

proof

let y be Element of L; :: 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 L such that
A4: y = x "/\" z and
A5: z in X by A3;
X is_<=_than sup X by A1, YELLOW_0:30;
then ( y <= z & z <= sup X ) by A4, A5, LATTICE3:def 9, YELLOW_0:23;
then ( y <= x & y <= sup X ) by A4, YELLOW_0:23, YELLOW_0:def 2;
hence y <= x "/\" (sup X) by YELLOW_0:23; :: thesis: verum

end;

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