let L1, L2 be non empty antisymmetric RelStr ; for D being Subset of [:L1,L2:] st ex_sup_of D,[:L1,L2:] holds
sup D = [(sup (proj1 D)),(sup (proj2 D))]
let D be Subset of [:L1,L2:]; ( ex_sup_of D,[:L1,L2:] implies sup D = [(sup (proj1 D)),(sup (proj2 D))] )
assume A1:
ex_sup_of D,[:L1,L2:]
; sup D = [(sup (proj1 D)),(sup (proj2 D))]
per cases
( D <> {} or D = {} )
;
suppose A2:
D = {}
;
sup D = [(sup (proj1 D)),(sup (proj2 D))]then
ex_sup_of {} ,
L2
by A1, FUNCT_5:8, YELLOW_3:41;
then A3:
L2 is
lower-bounded
by Th6;
ex_sup_of {} ,
L1
by A1, A2, FUNCT_5:8, YELLOW_3:41;
then
L1 is
lower-bounded
by Th6;
hence
sup D = [(sup (proj1 D)),(sup (proj2 D))]
by A1, A3, YELLOW10:5;
verum end; end;