let L be up-complete sup-Semilattice; :: thesis: for A, B being non empty directed Subset of L holds A is_<=_than sup (A "\/" B)
let A, B be non empty directed Subset of L; :: thesis: A is_<=_than sup (A "\/" B)
A1: A "\/" B = { (x "\/" y) where x, y is Element of L : ( x in A & y in B ) } by YELLOW_4:def 3;
set b = the Element of B;
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in A or x <= sup (A "\/" B) )
assume x in A ; :: thesis: x <= sup (A "\/" B)
then A2: x "\/" the Element of B in A "\/" B by A1;
ex xx being Element of L st
( x <= xx & the Element of B <= xx & ( for c being Element of L st x <= c & the Element of B <= c holds
xx <= c ) ) by LATTICE3:def 10;
then A3: x <= x "\/" the Element of B by LATTICE3:def 13;
ex_sup_of A "\/" B,L by WAYBEL_0:75;
then A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def 9;
then x "\/" the Element of B <= sup (A "\/" B) by A2;
hence x <= sup (A "\/" B) by A3, YELLOW_0:def 2; :: thesis: verum