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 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 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 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 A16, A18, Th15;
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 A16, A17, A18, WAYBEL_4:def 3; :: 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 A19, Th15; :: 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 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
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 A25, WAYBEL_4:def 3;
hence x <= w by A26, ORDERS_2:3; :: thesis: verum
end;
then y <= w by A22, YELLOW_0:def 9;
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
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 A9, A20;
for n being Nat holds S2[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;
hence y <= x by A22, YELLOW_0:def 9; :: thesis: verum
end;
SetBelow (R,C,y) is_<=_than y by Th16;
hence y = sup (SetBelow (R,C,y)) by A28, A27, YELLOW_0:def 9; :: thesis: verum