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

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