let L be non empty complete Poset; :: thesis:
let R be extra-order Relation of L; :: thesis:
let C be satisfying_SIC strict_chain of R; :: thesis:
let p, q be Element of L; :: thesis:
assume that
A1: p in C and
A2: q in C and
A3: p < q ; :: thesis:
A4: R satisfies_SIC_on C by Def7;
not q <= p by A3, ORDERS_2:30;
then not [q,p] in R by WAYBEL_4:def 4;
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, Th16;
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, Th16;
reconsider D = SetBelow R,C,w as non empty set by A9, A10, Th18;
defpred S₁[ set , set , set ] means ex a, b being Element of L st
( $2 = a & $3 = b & $3 in C & [$2,$3] in R & b <= w );
A12: for n being Element of NAT
for x being Element of D ex y being Element of D st S₁[n,x,y]

let n be Element of NAT ; :: thesis:
let x be Element of D; :: thesis:
x in D ;
then reconsider t = x as Element of L ;
A13: ( x in C & [x,w] in R ) by Th18;

per cases ;

suppose x <> w ; :: thesis:

then consider b being Element of L such that
A14: b in C and
A15: [x,b] in R and
A16: [b,w] in R and
t < b by A4, A5, A13, Th16;
reconsider y = b as Element of D by A14, A16, Th18;
take y ; :: thesis:
take t ; :: thesis:
take b ; :: thesis:
thus ( x = t & y = b & y in C & [x,y] in R & b <= w ) by A14, A15, A16, WAYBEL_4:def 4; :: thesis:

end;

suppose A17: x = w ; :: thesis:

take x ; :: thesis:
take t ; :: thesis:
take t ; :: thesis:
thus ( x = t & x = t & x in C & [x,x] in R & t <= w ) by A17, Th18; :: thesis:

end;

reconsider g = x1 as Element of D by A9, A10, Th18;
consider f being Function of NAT ,D such that
A18: f . 0 = g and
A19: for n being Element of NAT holds S₁[n,f . n,f . (n + 1)] from RECDEF_1:sch 2(A12);
reconsider f = f as Function of NAT ,the carrier of L by FUNCT_2:9;
take y = sup (rng f); :: thesis:
A20: ex_sup_of rng f,L by YELLOW_0:17;
A21: dom f = NAT by FUNCT_2:def 1;
then x1 <= y by A18, A20, FUNCT_1:12, YELLOW_4:1;
hence p < y by A11, ORDERS_2:32; :: thesis:
A22: q <= q ;
rng f is_<=_than w

let x be Element of L; :: according to LATTICE3:def 9 :: thesis:
assume x in rng f ; :: thesis:
then consider n being set such that
A23: n in dom f and
A24: f . n = x by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A23;
A25: ex a, b being Element of L st
( f . n = a & f . (n + 1) = b & f . (n + 1) in C & [(f . n),(f . (n + 1))] in R & b <= w ) by A19;
then x <= f . (n + 1) by A24, WAYBEL_4:def 4;
hence x <= w by A25, ORDERS_2:26; :: thesis:

end;

then y <= w by A20, YELLOW_0:def 9;
hence [y,q] in R by A7, A22, WAYBEL_4:def 5; :: thesis:
A26: ex_sup_of SetBelow R,C,y,L by YELLOW_0:17;
A27: SetBelow R,C,y is_<=_than y by Th19;
for x being Element of L st SetBelow R,C,y is_<=_than x holds
y <= x

let x be Element of L; :: thesis:
assume A28: SetBelow R,C,y is_<=_than x ; :: thesis:
rng f is_<=_than x

let m be Element of L; :: according to LATTICE3:def 9 :: thesis:
assume m in rng f ; :: thesis:
then consider n being set such that
A29: n in dom f and
A30: f . n = m by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A29;
A31: ex a, b being Element of L st
( f . n = a & f . (n + 1) = b & f . (n + 1) in C & [(f . n),(f . (n + 1))] in R & b <= w ) by A19;
defpred S₂[ Nat] means f . $1 in C;
for n being Nat holds S₂[n]

A32: S₂[ 0 ] by A9, A18;
A33: for k being Nat st S₂[k] holds
S₂[k + 1]

let k be Nat; :: thesis:
k is Element of NAT by ORDINAL1:def 13;
then ex a, b being Element of L st
( f . k = a & f . (k + 1) = b & f . (k + 1) in C & [(f . k),(f . (k + 1))] in R & b <= w ) by A19;
hence ( S₂[k] implies S₂[k + 1] ) ; :: thesis:

end;

thus for n being Nat holds S₂[n] from NAT_1:sch 2(A32, A33); :: thesis:

end;

then A34: f . n in C ;
A35: f . n <= f . n ;
f . (n + 1) <= y by A20, A21, FUNCT_1:12, YELLOW_4:1;
then [m,y] in R by A30, A31, A35, WAYBEL_4:def 5;
then m in SetBelow R,C,y by A30, A34, Th18;
hence m <= x by A28, LATTICE3:def 9; :: thesis:

end;

hence y <= x by A20, YELLOW_0:def 9; :: thesis:

end;

hence y = sup (SetBelow R,C,y) by A26, A27, YELLOW_0:def 9; :: thesis: