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

let q be Element of L; :: according to LATTICE3:def 8 :: thesis:
assume q in {x} "\/" X ; :: thesis:
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:

end;