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 A3, ORDERS_2:6;

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 S_{1}[ 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 A9, A10, Th15;

reconsider g = x1 as Element of D by A9, A10, Th15;

A13: for n being Nat

for x being Element of D ex y being Element of D st S_{1}[n,x,y]

A20: f . 0 = g and

A21: for n being Nat holds S_{1}[n,f . n,f . (n + 1)]
from RECDEF_1:sch 2(A13);

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 A20, A22, FUNCT_1:3, YELLOW_4:1;

hence p < y by A11, ORDERS_2:7; :: thesis: ( [y,q] in R & y = sup (SetBelow (R,C,y)) )

rng f is_<=_than w

hence [y,q] in R by A7, A12, WAYBEL_4:def 4; :: 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

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

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 A3, ORDERS_2:6;

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 S

( $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 A9, A10, Th15;

reconsider g = x1 as Element of D by A9, A10, Th15;

A13: for n being Nat

for x being Element of D ex y being Element of D st S

proof

consider f being sequence of D such that
let n be Nat; :: thesis: for x being Element of D ex y being Element of D st S_{1}[n,x,y]

let x be Element of D; :: thesis: ex y being Element of D st S_{1}[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;

end;let x be Element of D; :: thesis: ex y being Element of D st S

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 )
;

end;

suppose
x <> w
; :: thesis: ex y being Element of D st S_{1}[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 A16, A18, Th15;

take y ; :: thesis: S_{1}[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 A16, A17, A18, WAYBEL_4:def 3; :: thesis: verum

end;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 A16, A18, Th15;

take y ; :: thesis: S

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 A16, A17, A18, WAYBEL_4:def 3; :: thesis: verum

A20: f . 0 = g and

A21: for n being Nat holds S

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 A20, A22, FUNCT_1:3, YELLOW_4:1;

hence p < y by A11, ORDERS_2:7; :: thesis: ( [y,q] in R & y = sup (SetBelow (R,C,y)) )

rng f is_<=_than w

proof

then
y <= w
by A22, YELLOW_0:def 9;
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 A25, WAYBEL_4:def 3;

hence x <= w by A26, ORDERS_2:3; :: thesis: verum

end;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 A25, WAYBEL_4:def 3;

hence x <= w by A26, ORDERS_2:3; :: thesis: verum

hence [y,q] in R by A7, A12, WAYBEL_4:def 4; :: 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

SetBelow (R,C,y) is_<=_than y
by Th16;
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

end;assume A29: SetBelow (R,C,y) is_<=_than x ; :: thesis: y <= x

rng f is_<=_than x

proof

hence
y <= x
by A22, YELLOW_0:def 9; :: thesis: verum
defpred S_{2}[ 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 S_{2}[k] holds

S_{2}[k + 1]
_{2}[ 0 ]
by A9, A20;

for n being Nat holds S_{2}[n]
from NAT_1:sch 2(A34, A33);

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 A22, A23, FUNCT_1:3, YELLOW_4:1;

then [m,y] in R by A31, A36, A32, WAYBEL_4:def 4;

then m in SetBelow (R,C,y) by A31, A35, Th15;

hence m <= x by A29; :: thesis: verum

end;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 S

S

proof

A34:
S
let k be Nat; :: thesis: ( S_{2}[k] implies S_{2}[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 ( S_{2}[k] implies S_{2}[k + 1] )
; :: thesis: verum

end;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 ( S

for n being Nat holds S

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 A22, A23, FUNCT_1:3, YELLOW_4:1;

then [m,y] in R by A31, A36, A32, WAYBEL_4:def 4;

then m in SetBelow (R,C,y) by A31, A35, Th15;

hence m <= x by A29; :: thesis: verum

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