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 B,L by WAYBEL_0:75;
then A2: B is_<=_than sup B by YELLOW_0:30;
A3: ex_sup_of A,L by WAYBEL_0:75;
then A is_<=_than sup A by YELLOW_0:30;
then ( ex_sup_of A "\/" B,L & A "\/" B is_<=_than (sup A) "\/" (sup B) ) by A2, WAYBEL_0:75, YELLOW_4:27;
then A4: sup (A "\/" B) <= (sup A) "\/" (sup B) by YELLOW_0:def 9;
B is_<=_than sup (A "\/" B) by Th3;
then A5: sup B <= sup (A "\/" B) by A1, YELLOW_0:30;
A is_<=_than sup (A "\/" B) by Th3;
then sup A <= sup (A "\/" B) by A3, YELLOW_0:30;
then A6: (sup A) "\/" (sup B) <= (sup (A "\/" B)) "\/" (sup (A "\/" B)) by A5, 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 A4, A6, ORDERS_2:2; :: thesis: verum