let L be non empty reflexive antisymmetric up-complete RelStr ; :: thesis: 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:]; :: thesis: 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

D1 is_<=_than d1

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; :: thesis: verum

let D be non empty directed Subset of [:L,L:]; :: thesis: 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

proof

then A7:
sup D2 <= d2
by A4, YELLOW_0:def 9;
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in D2 or b <= d2 )

assume b in D2 ; :: thesis: b <= d2

then consider x being object such that

A6: [x,b] in D by XTUPLE_0:def 13;

reconsider x = x as Element of D1 by A6, XTUPLE_0:def 12;

D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def 9;

then [x,b] <= [d1,d2] by A6;

hence b <= d2 by YELLOW_3:11; :: thesis: verum

end;assume b in D2 ; :: thesis: b <= d2

then consider x being object such that

A6: [x,b] in D by XTUPLE_0:def 13;

reconsider x = x as Element of D1 by A6, XTUPLE_0:def 12;

D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def 9;

then [x,b] <= [d1,d2] by A6;

hence b <= d2 by YELLOW_3:11; :: thesis: verum

D1 is_<=_than d1

proof

then
sup D1 <= d1
by A1, YELLOW_0:def 9;
let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in D1 or b <= d1 )

assume b in D1 ; :: thesis: b <= d1

then consider x being object such that

A8: [b,x] in D by XTUPLE_0:def 12;

reconsider x = x as Element of D2 by A8, XTUPLE_0:def 13;

D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def 9;

then [b,x] <= [d1,d2] by A8;

hence b <= d1 by YELLOW_3:11; :: thesis: verum

end;assume b in D1 ; :: thesis: b <= d1

then consider x being object such that

A8: [b,x] in D by XTUPLE_0:def 12;

reconsider x = x as Element of D2 by A8, XTUPLE_0:def 13;

D is_<=_than [d1,d2] by A5, A3, YELLOW_0:def 9;

then [b,x] <= [d1,d2] by A8;

hence b <= d1 by YELLOW_3:11; :: thesis: verum

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; :: thesis: verum