let L be up-complete sup-Semilattice; 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; 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; verum