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)
B is_<=_than sup (A "\/" B) by Th25;
then A1: sup B <= sup (A "\/" B) by YELLOW_0:32;
A is_<=_than sup (A "\/" B) by Th25;
then sup A <= sup (A "\/" B) by YELLOW_0:32;
then A2: (sup A) "\/" (sup B) <= (sup (A "\/" B)) "\/" (sup (A "\/" B)) by A1, YELLOW_3:3;
( A is_<=_than sup A & B is_<=_than sup B ) by YELLOW_0:32;
then ( ex_sup_of A "\/" B,L & A "\/" B is_<=_than (sup A) "\/" (sup B) ) by Th27, YELLOW_0:17;
then A3: sup (A "\/" B) <= (sup A) "\/" (sup B) by YELLOW_0:def 9;
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, A2, ORDERS_2:2; :: thesis: verum