let k, k9 be Nat; :: thesis: for d being non zero Nat
for l, r, l9, r9 being Element of REAL d
for G being Grating of d st k < k9 & k9 <= d & cell (l,r) in cells (k,G) & cell (l9,r9) in cells (k9,G) & cell (l,r) c= cell (l9,r9) holds
ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )
let d be non zero Nat; :: thesis: for l, r, l9, r9 being Element of REAL d
for G being Grating of d st k < k9 & k9 <= d & cell (l,r) in cells (k,G) & cell (l9,r9) in cells (k9,G) & cell (l,r) c= cell (l9,r9) holds
ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )
let l, r, l9, r9 be Element of REAL d; :: thesis: for G being Grating of d st k < k9 & k9 <= d & cell (l,r) in cells (k,G) & cell (l9,r9) in cells (k9,G) & cell (l,r) c= cell (l9,r9) holds
ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )
let G be Grating of d; :: thesis: ( k < k9 & k9 <= d & cell (l,r) in cells (k,G) & cell (l9,r9) in cells (k9,G) & cell (l,r) c= cell (l9,r9) implies ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) )
assume that
A1: k < k9 and
A2: k9 <= d and
A3: cell (l,r) in cells (k,G) and
A4: cell (l9,r9) in cells (k9,G) ; :: thesis: ( not cell (l,r) c= cell (l9,r9) or ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) )
A5: k + 0 < d by A1, A2, XXREAL_0:2;
assume A6: cell (l,r) c= cell (l9,r9) ; :: thesis: ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )
consider X being Subset of (Seg d) such that
A7: card X = k and
A8: for i being Element of Seg d holds
( ( i in X & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in X & l . i = r . i & l . i in G . i ) ) by A3, A5, Th30;
A9: d - k > 0 by A5, XREAL_1:20;
card ((Seg d) \ X) = (card (Seg d)) - (card X) by CARD_2:44
.= d - k by A7, FINSEQ_1:57 ;
then consider i0 being object such that
A10: i0 in (Seg d) \ X by A9, CARD_1:27, XBOOLE_0:def 1;
reconsider i0 = i0 as Element of Seg d by A10, XBOOLE_0:def 5;
not i0 in X by A10, XBOOLE_0:def 5;
then A11: l . i0 = r . i0 by A8;
per cases ( ( l . i0 = l9 . i0 & r . i0 = r9 . i0 ) or ( l . i0 = l9 . i0 & r . i0 = l9 . i0 ) or ( l . i0 = r9 . i0 & r . i0 = r9 . i0 ) or r9 . i0 < l9 . i0 ) by A2, A3, A4, A5, A6, Th42;
suppose ( l . i0 = l9 . i0 & r . i0 = r9 . i0 ) ; :: thesis: ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )
hence ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) by A11; :: thesis: verum
end;
suppose ( l . i0 = l9 . i0 & r . i0 = l9 . i0 ) ; :: thesis: ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )
hence ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) ; :: thesis: verum
end;
suppose ( l . i0 = r9 . i0 & r . i0 = r9 . i0 ) ; :: thesis: ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )
hence ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) ; :: thesis: verum
end;
suppose A12: r9 . i0 < l9 . i0 ; :: thesis: ex i being Element of Seg d st
( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) )
assume A13: for i being Element of Seg d holds
( ( l . i <> l9 . i or r . i <> l9 . i ) & ( l . i <> r9 . i or r . i <> r9 . i ) ) ; :: thesis: contradiction
defpred S1[ Element of Seg d, Element of REAL ] means ( l . $1 <= $2 & $2 <= r . $1 & r9 . $1 < $2 & $2 < l9 . $1 );
A14: for i being Element of Seg d ex xi being Element of REAL st S1[i,xi]
proof
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S1[i,xi]
A15: l . i in G . i by A3, A5, Th32;
A16: r . i in G . i by A3, A5, Th32;
A17: r9 . i < l9 . i by A2, A4, A12, Th31;
A18: [(l9 . i),(r9 . i)] is Gap of G . i by A2, A4, A12, Th31;
per cases ( ( r9 . i < l . i & l . i < l9 . i ) or l . i <= r9 . i or l9 . i <= l . i ) ;
suppose A19: ( r9 . i < l . i & l . i < l9 . i ) ; :: thesis: ex xi being Element of REAL st S1[i,xi]
reconsider li = l . i as Element of REAL by XREAL_0:def 1;
take li ; :: thesis: S1[i,li]
thus S1[i,li] by A8, A19; :: thesis: verum
end;
suppose A20: l . i <= r9 . i ; :: thesis: ex xi being Element of REAL st S1[i,xi]
A21: l . i >= r9 . i by A15, A17, A18, Th13;
then A22: l . i = r9 . i by A20, XXREAL_0:1;
then r . i <> r9 . i by A13;
then l . i < r . i by A8, A22;
then consider xi being Element of REAL such that
A23: l . i < xi and
A24: xi < r . i by Th1;
take xi ; :: thesis: S1[i,xi]
r . i <= l9 . i by A16, A17, A18, Th13;
hence S1[i,xi] by A21, A23, A24, XXREAL_0:2; :: thesis: verum
end;
suppose A25: l9 . i <= l . i ; :: thesis: ex xi being Element of REAL st S1[i,xi]
l9 . i >= l . i by A15, A17, A18, Th13;
then A26: l9 . i = l . i by A25, XXREAL_0:1;
l9 . i >= r . i by A16, A17, A18, Th13;
then l9 . i = r . i by A8, A26;
hence ex xi being Element of REAL st S1[i,xi] by A13, A26; :: thesis: verum
end;
end;
end;
consider x being Function of (Seg d),REAL such that
A27: for i being Element of Seg d holds S1[i,x . i] from FUNCT_2:sch 3(A14);
reconsider x = x as Element of REAL d by Def3;
A28: x in cell (l,r) by A27;
for i being Element of Seg d st r9 . i < l9 . i holds
( r9 . i < x . i & x . i < l9 . i ) by A27;
hence contradiction by A6, A12, A28, Th22; :: thesis: verum
end;
end;