let L be non empty complete Poset; :: thesis: for R being extra-order Relation of L
for C being satisfying_SIC strict_chain of R
for a, b being Element of L st a in C & b in C & a < b holds
ex d being Element of L st
( d in SupBelow R,C & a < d & [d,b] in R )
let R be extra-order Relation of L; :: thesis: for C being satisfying_SIC strict_chain of R
for a, b being Element of L st a in C & b in C & a < b holds
ex d being Element of L st
( d in SupBelow R,C & a < d & [d,b] in R )
let C be satisfying_SIC strict_chain of R; :: thesis: for a, b being Element of L st a in C & b in C & a < b holds
ex d being Element of L st
( d in SupBelow R,C & a < d & [d,b] in R )
let a, b be Element of L; :: thesis: ( a in C & b in C & a < b implies ex d being Element of L st
( d in SupBelow R,C & a < d & [d,b] in R ) )
assume ( a in C & b in C & a < b ) ; :: thesis: ex d being Element of L st
( d in SupBelow R,C & a < d & [d,b] in R )
then consider d being Element of L such that
A1: ( a < d & [d,b] in R & d = sup (SetBelow R,C,d) ) by Th22;
take d ; :: thesis: ( d in SupBelow R,C & a < d & [d,b] in R )
thus ( d in SupBelow R,C & a < d & [d,b] in R ) by A1, Def10; :: thesis: verum