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;
A6: y <= z by A4, YELLOW_0:23;
X is_<=_than sup X by A1, YELLOW_0:30;
then z <= sup X by A5;
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