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 that
A1: a in C and
A2: b in C and
A3: a < b ; :: thesis: ex d being Element of L st
( d in SupBelow (R,C) & a < d & [d,b] in R )
consider d being Element of L such that
A4: a < d and
A5: [d,b] in R and
A6: d = sup (SetBelow (R,C,d)) by A1, A2, A3, Th19;
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 A4, A5, A6, Def10; :: thesis: verum