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)

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

hence
x "/\" (sup X) >= sup Y
by A2, YELLOW_0:30; :: thesis: verum
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;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