let L be up-complete sup-Semilattice; :: thesis: for A, B being non empty directed Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)
let A, B be non empty directed Subset of L; :: thesis: sup (A "\/" B) = (sup A) "\/" (sup B)
A1: ex_sup_of A "\/" B,L by WAYBEL_0:75;
A2: ( ex_sup_of A,L & ex_sup_of B,L ) by WAYBEL_0:75;
then ( A is_<=_than sup A & B is_<=_than sup B ) by YELLOW_0:30;
then A "\/" B is_<=_than (sup A) "\/" (sup B) by YELLOW_4:27;
then A3: sup (A "\/" B) <= (sup A) "\/" (sup B) by A1, YELLOW_0:def 9;
( A is_<=_than sup (A "\/" B) & B is_<=_than sup (A "\/" B) ) by Th3;
then ( sup A <= sup (A "\/" B) & sup B <= sup (A "\/" B) ) by A2, YELLOW_0:30;
then A4: (sup A) "\/" (sup B) <= (sup (A "\/" B)) "\/" (sup (A "\/" B)) by YELLOW_3:3;
sup (A "\/" B) <= sup (A "\/" B) ;
then (sup (A "\/" B)) "\/" (sup (A "\/" B)) = sup (A "\/" B) by YELLOW_0:24;
hence sup (A "\/" B) = (sup A) "\/" (sup B) by A3, A4, ORDERS_2:25; :: thesis: verum