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;
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 :: thesis: ( c < sup (SetBelow (R,C,c)) implies c = sup (SetBelow (R,C,c)) )
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 6;
hence c <= a by A11, ORDERS_2:3; :: thesis: verum
end;
SetBelow (R,C,c) is_<=_than c by Th16;
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 3;
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, Th13, ORDERS_2:def 6;
y in SetBelow (R,C,c) by A12, A13, Th15;
hence c = sup (SetBelow (R,C,c)) by A5, A14, ORDERS_2:6, YELLOW_4:1; :: thesis: verum
end;
end;