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 and
A4: a in {x} and
b in D by A1;
a = x by A4, TARSKI:def 1;
hence c <= x by A3, YELLOW_0:23; :: thesis: verum
end;
then x is_>=_than {x} "/\" D ;
hence sup ({x} "/\" D) <= x by A2, YELLOW_0:30; :: thesis: verum