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;
ex_sup_of A "\/" B,L by WAYBEL_0:75;
then A2: A "\/" B is_<=_than sup (A "\/" B) by YELLOW_0:def 9;
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in A or x <= sup (A "\/" B) )
assume A3: x in A ; :: thesis: x <= sup (A "\/" B)
consider b being Element of B;
x "\/" b in A "\/" B by A1, A3;
then A4: x "\/" b <= sup (A "\/" B) by A2, LATTICE3:def 9;
ex xx being Element of L st
( x <= xx & b <= xx & ( for c being Element of L st x <= c & b <= c holds
xx <= c ) ) by LATTICE3:def 10;
then x <= x "\/" b by LATTICE3:def 13;
hence x <= sup (A "\/" B) by A4, YELLOW_0:def 2; :: thesis: verum