let L be non empty lower-bounded Poset; :: thesis: for R being extra-order Relation of L
for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds
ex_sup_of SetBelow R,C,c,L ) & R satisfies_SIC_on C holds
for c being Element of L st c in C holds
c = sup (SetBelow R,C,c)
let R be extra-order Relation of L; :: thesis: for C being non empty strict_chain of R st C is sup-closed & ( for c being Element of L st c in C holds
ex_sup_of SetBelow R,C,c,L ) & R satisfies_SIC_on C holds
for c being Element of L st c in C holds
c = sup (SetBelow R,C,c)
let C be non empty strict_chain of R; :: thesis: ( C is sup-closed & ( for c being Element of L st c in C holds
ex_sup_of SetBelow R,C,c,L ) & R satisfies_SIC_on C implies for c being Element of L st c in C holds
c = sup (SetBelow R,C,c) )
assume that
A1: C is sup-closed and
A2: for c being Element of L st c in C holds
ex_sup_of SetBelow R,C,c,L ; :: thesis: ( not R satisfies_SIC_on C or for c being Element of L st c in C holds
c = sup (SetBelow R,C,c) )
assume A3: R satisfies_SIC_on C ; :: thesis: for c being Element of L st c in C holds
c = sup (SetBelow R,C,c)
let c be Element of L; :: thesis: ( c in C implies c = sup (SetBelow R,C,c) )
assume A4: c in C ; :: thesis: c = sup (SetBelow R,C,c)
A5: ex_sup_of SetBelow R,C,c,L by A2, A4;
set d = sup (SetBelow R,C,c);
SetBelow R,C,c c= C by XBOOLE_1:17;
then sup (SetBelow R,C,c) = "\/" (SetBelow R,C,c),(subrelstr C) by A1, A5, Def9;
then sup (SetBelow R,C,c) in the carrier of (subrelstr C) ;
then A6: sup (SetBelow R,C,c) in C by YELLOW_0:def 15;

per cases ( c = sup (SetBelow R,C,c) or c <> sup (SetBelow R,C,c) ) ;

suppose c = sup (SetBelow R,C,c) ; :: thesis: c = sup (SetBelow R,C,c)

hence c = sup (SetBelow R,C,c) ; :: thesis: verum

end;

suppose A7: c <> sup (SetBelow R,C,c) ; :: thesis: c = sup (SetBelow R,C,c)

A8: now

assume A9: c < sup (SetBelow R,C,c) ; :: thesis: c = sup (SetBelow R,C,c)
A10: for a being Element of L st SetBelow R,C,c is_<=_than a holds
c <= a

proof

let a be Element of L; :: thesis: ( SetBelow R,C,c is_<=_than a implies c <= a )
assume SetBelow R,C,c is_<=_than a ; :: thesis: c <= a
then A11: sup (SetBelow R,C,c) <= a by A5, YELLOW_0:def 9;
c <= sup (SetBelow R,C,c) by A9, ORDERS_2:def 10;
hence c <= a by A11, ORDERS_2:26; :: thesis: verum

end;

SetBelow R,C,c is_<=_than c by Th19;
hence c = sup (SetBelow R,C,c) by A10, A5, YELLOW_0:def 9; :: thesis: verum

end;

( [c,(sup (SetBelow R,C,c))] in R or [(sup (SetBelow R,C,c)),c] in R ) by A7, A4, A6, Def3;
then ( c <= sup (SetBelow R,C,c) or [(sup (SetBelow R,C,c)),c] in R ) by WAYBEL_4:def 4;
then consider y being Element of L such that
A12: y in C and
[(sup (SetBelow R,C,c)),y] in R and
A13: [y,c] in R and
A14: sup (SetBelow R,C,c) < y by A8, A3, A4, A6, A7, Th16, ORDERS_2:def 10;
y in SetBelow R,C,c by A12, A13, Th18;
hence c = sup (SetBelow R,C,c) by A5, A14, ORDERS_2:30, YELLOW_4:1; :: thesis: verum

end;

end;