let L be complete LATTICE; :: thesis: for x being Element of L
for D being directed Subset of L holds sup ({x} "/\" D) <= x
let x be Element of L; :: thesis: for D being directed Subset of L holds sup ({x} "/\" D) <= x
let D be directed Subset of L; :: thesis: sup ({x} "/\" D) <= x
A1: {x} "/\" D = { (a "/\" b) where a, b is Element of L : ( a in {x} & b in D ) } by YELLOW_4:def 4;
A2: ex_sup_of {x} "/\" D,L by YELLOW_0:17;
for c being Element of L st c in {x} "/\" D holds
c <= x

proof

let c be Element of L; :: thesis: ( c in {x} "/\" D implies c <= x )
assume c in {x} "/\" D ; :: thesis: c <= x
then consider a, b being Element of L such that
A3: ( c = a "/\" b & a in {x} & b in D ) by A1;
a = x by A3, TARSKI:def 1;
hence c <= x by A3, YELLOW_0:23; :: thesis: verum

end;

then x is_>=_than {x} "/\" D by LATTICE3:def 9;
hence sup ({x} "/\" D) <= x by A2, YELLOW_0:30; :: thesis: verum