let L be with_suprema Poset; :: thesis: for X being Subset of L
for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds
x "\/" (inf X) <= inf ({x} "\/" X)
let X be Subset of L; :: thesis: for x being Element of L st ex_inf_of {x} "\/" X,L & ex_inf_of X,L holds
x "\/" (inf X) <= inf ({x} "\/" X)
let x be Element of L; :: thesis: ( ex_inf_of {x} "\/" X,L & ex_inf_of X,L implies x "\/" (inf X) <= inf ({x} "\/" X) )
assume that
A1: ex_inf_of {x} "\/" X,L and
A2: ex_inf_of X,L ; :: thesis: x "\/" (inf X) <= inf ({x} "\/" X)
A3: {x} "\/" X = { (x "\/" y) where y is Element of L : y in X } by Th15;
{x} "\/" X is_>=_than x "\/" (inf X)

proof

let q be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not q in {x} "\/" X or x "\/" (inf X) <= q )
assume q in {x} "\/" X ; :: thesis: x "\/" (inf X) <= q
then consider y being Element of L such that
A4: q = x "\/" y and
A5: y in X by A3;
( x <= x & y >= inf X ) by A2, A5, Th2;
hence x "\/" (inf X) <= q by A4, YELLOW_3:3; :: thesis: verum

end;

hence x "\/" (inf X) <= inf ({x} "\/" X) by A1, YELLOW_0:def 10; :: thesis: verum