let L be Semilattice; :: thesis:
let X be Subset of L; :: thesis:
let x be Element of L; :: thesis:
assume that
A1: ex_sup_of {x} "/\" X,L and
A2: ex_sup_of X,L ; :: thesis:
A3: {x} "/\" X = { (x "/\" y) where y is Element of L : y in X } by Th42;
{x} "/\" X is_<=_than x "/\" (sup X)

let q be Element of L; :: according to LATTICE3:def 9 :: 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 <= sup X ) by A2, A5, Th1;
hence q <= x "/\" (sup X) by A4, YELLOW_3:2; :: thesis:

end;