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 p, q being Element of L st p in C & q in C & p < q holds
ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )

let R be extra-order Relation of L; :: thesis: for C being satisfying_SIC strict_chain of R
for p, q being Element of L st p in C & q in C & p < q holds
ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )

let C be satisfying_SIC strict_chain of R; :: thesis: for p, q being Element of L st p in C & q in C & p < q holds
ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )

let p, q be Element of L; :: thesis: ( p in C & q in C & p < q implies ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) ) )

assume that
A1: p in C and
A2: q in C and
A3: p < q ; :: thesis: ex y being Element of L st
( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )

A4: R satisfies_SIC_on C by Def7;
not q <= p by ;
then not [q,p] in R by WAYBEL_4:def 3;
then [p,q] in R by A1, A2, A3, Def3;
then consider w being Element of L such that
A5: w in C and
A6: [p,w] in R and
A7: [w,q] in R and
A8: p < w by A1, A2, A3, A4, Th13;
consider x1 being Element of L such that
A9: x1 in C and
[p,x1] in R and
A10: [x1,w] in R and
A11: p < x1 by A1, A4, A5, A6, A8, Th13;
defpred S1[ set , set , set ] means ex b being Element of L st
( \$3 = b & \$3 in C & [\$2,\$3] in R & b <= w );
A12: q <= q ;
reconsider D = SetBelow (R,C,w) as non empty set by ;
reconsider g = x1 as Element of D by ;
A13: for n being Nat
for x being Element of D ex y being Element of D st S1[n,x,y]
proof
let n be Nat; :: thesis: for x being Element of D ex y being Element of D st S1[n,x,y]
let x be Element of D; :: thesis: ex y being Element of D st S1[n,x,y]
x in D ;
then reconsider t = x as Element of L ;
A14: x in C by Th15;
A15: [x,w] in R by Th15;
per cases ( x <> w or x = w ) ;
suppose x <> w ; :: thesis: ex y being Element of D st S1[n,x,y]
then consider b being Element of L such that
A16: b in C and
A17: [x,b] in R and
A18: [b,w] in R and
t < b by A4, A5, A14, A15, Th13;
reconsider y = b as Element of D by ;
take y ; :: thesis: S1[n,x,y]
take b ; :: thesis: ( y = b & y in C & [x,y] in R & b <= w )
thus ( y = b & y in C & [x,y] in R & b <= w ) by ; :: thesis: verum
end;
suppose A19: x = w ; :: thesis: ex y being Element of D st S1[n,x,y]
take x ; :: thesis: S1[n,x,x]
take t ; :: thesis: ( x = t & x in C & [x,x] in R & t <= w )
thus ( x = t & x in C & [x,x] in R & t <= w ) by ; :: thesis: verum
end;
end;
end;
consider f being sequence of D such that
A20: f . 0 = g and
A21: for n being Nat holds S1[n,f . n,f . (n + 1)] from reconsider f = f as sequence of the carrier of L by FUNCT_2:7;
take y = sup (rng f); :: thesis: ( p < y & [y,q] in R & y = sup (SetBelow (R,C,y)) )
A22: ex_sup_of rng f,L by YELLOW_0:17;
A23: dom f = NAT by FUNCT_2:def 1;
then x1 <= y by ;
hence p < y by ; :: thesis: ( [y,q] in R & y = sup (SetBelow (R,C,y)) )
rng f is_<=_than w
proof
let x be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not x in rng f or x <= w )
assume x in rng f ; :: thesis: x <= w
then consider n being object such that
A24: n in dom f and
A25: f . n = x by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A24;
A26: ex b being Element of L st
( f . (n + 1) = b & f . (n + 1) in C & [(f . n),(f . (n + 1))] in R & b <= w ) by A21;
then x <= f . (In ((n + 1),NAT)) by ;
hence x <= w by ; :: thesis: verum
end;
then y <= w by ;
hence [y,q] in R by ; :: thesis: y = sup (SetBelow (R,C,y))
A27: ex_sup_of SetBelow (R,C,y),L by YELLOW_0:17;
A28: for x being Element of L st SetBelow (R,C,y) is_<=_than x holds
y <= x
proof
let x be Element of L; :: thesis: ( SetBelow (R,C,y) is_<=_than x implies y <= x )
assume A29: SetBelow (R,C,y) is_<=_than x ; :: thesis: y <= x
rng f is_<=_than x
proof
defpred S2[ Nat] means f . \$1 in C;
let m be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not m in rng f or m <= x )
assume m in rng f ; :: thesis: m <= x
then consider n being object such that
A30: n in dom f and
A31: f . n = m by FUNCT_1:def 3;
reconsider n = n as Element of NAT by A30;
A32: f . n <= f . n ;
A33: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
ex b being Element of L st
( f . (k + 1) = b & f . (k + 1) in C & [(f . k),(f . (k + 1))] in R & b <= w ) by A21;
hence ( S2[k] implies S2[k + 1] ) ; :: thesis: verum
end;
A34: S2[ 0 ] by ;
for n being Nat holds S2[n] from then A35: f . n in C ;
A36: ex b being Element of L st
( f . (n + 1) = b & f . (n + 1) in C & [(f . n),(f . (n + 1))] in R & b <= w ) by A21;
f . (In ((n + 1),NAT)) <= y by ;
then [m,y] in R by ;
then m in SetBelow (R,C,y) by ;
hence m <= x by A29; :: thesis: verum
end;
hence y <= x by ; :: thesis: verum
end;
SetBelow (R,C,y) is_<=_than y by Th16;
hence y = sup (SetBelow (R,C,y)) by ; :: thesis: verum