let L be non empty complete Poset; 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; 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; 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; ( 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
; 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
; ( 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; verum