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

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