let L be non empty reflexive antisymmetric up-complete RelStr ; for D being non empty directed Subset of [:L,L:] holds sup D = [(sup (proj1 D)),(sup (proj2 D))]
let D be non empty directed Subset of [:L,L:]; sup D = [(sup (proj1 D)),(sup (proj2 D))]
reconsider D1 = proj1 D, D2 = proj2 D as non empty directed Subset of L by YELLOW_3:21, YELLOW_3:22;
reconsider C = the carrier of L as non empty set ;
reconsider D9 = D as non empty Subset of [:C,C:] by YELLOW_3:def 2;
A1:
ex_sup_of D1,L
by WAYBEL_0:75;
the carrier of [:L,L:] = [:C,C:]
by YELLOW_3:def 2;
then consider d1, d2 being object such that
A2:
( d1 in C & d2 in C )
and
A3:
sup D = [d1,d2]
by ZFMISC_1:def 2;
A4:
ex_sup_of D2,L
by WAYBEL_0:75;
reconsider d1 = d1, d2 = d2 as Element of L by A2;
A5:
ex_sup_of D,[:L,L:]
by WAYBEL_0:75;
D2 is_<=_than d2
then A7:
sup D2 <= d2
by A4, YELLOW_0:def 9;
D1 is_<=_than d1
then
sup D1 <= d1
by A1, YELLOW_0:def 9;
then A9:
[(sup D1),(sup D2)] <= sup D
by A3, A7, YELLOW_3:11;
A10:
ex_sup_of [:D1,D2:],[:L,L:]
by WAYBEL_0:75;
reconsider D1 = D1, D2 = D2 as non empty Subset of L ;
D9 c= [:D1,D2:]
by YELLOW_3:1;
then
sup D <= sup [:D1,D2:]
by A5, A10, YELLOW_0:34;
then
sup D <= [(sup (proj1 D)),(sup (proj2 D))]
by A1, A4, YELLOW_3:43;
hence
sup D = [(sup (proj1 D)),(sup (proj2 D))]
by A9, ORDERS_2:2; verum