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

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