let L be non empty complete Poset; :: thesis: for A, B being non empty Subset of L holds sup (A "\/" B) = (sup A) "\/" (sup B)
let A, B be non empty Subset of L; :: thesis: sup (A "\/" B) = (sup A) "\/" (sup B)
A1: ex_sup_of A "\/" B,L by YELLOW_0:17;
( A is_<=_than sup A & B is_<=_than sup B ) by YELLOW_0:32;
then A "\/" B is_<=_than (sup A) "\/" (sup B) by Th27;
then A2: 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 Th25;
then ( sup A <= sup (A "\/" B) & sup B <= sup (A "\/" B) ) by YELLOW_0:32;
then A3: (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 A2, A3, ORDERS_2:25; :: thesis: verum