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;

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;

end;

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

( ( 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;( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) by A11; :: thesis: verum

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

( ( 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;( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) ; :: thesis: verum

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

( ( 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;( ( l . i = l9 . i & r . i = l9 . i ) or ( l . i = r9 . i & r . i = r9 . i ) ) ; :: thesis: verum

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

( ( 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 S_{1}[ 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 S_{1}[i,xi]

A27: for i being Element of Seg d holds S_{1}[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;( ( l . i <> l9 . i or r . i <> l9 . i ) & ( l . i <> r9 . i or r . i <> r9 . i ) ) ; :: thesis: contradiction

defpred S

A14: for i being Element of Seg d ex xi being Element of REAL st S

proof

consider x being Function of (Seg d),REAL such that
let i be Element of Seg d; :: thesis: ex xi being Element of REAL st S_{1}[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;

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

end;

suppose A19:
( r9 . i < l . i & l . i < l9 . i )
; :: thesis: ex xi being Element of REAL st S_{1}[i,xi]

reconsider li = l . i as Element of REAL by XREAL_0:def 1;

take li ; :: thesis: S_{1}[i,li]

thus S_{1}[i,li]
by A8, A19; :: thesis: verum

end;take li ; :: thesis: S

thus S

suppose A20:
l . i <= r9 . i
; :: thesis: ex xi being Element of REAL st S_{1}[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: S_{1}[i,xi]

r . i <= l9 . i by A16, A17, A18, Th13;

hence S_{1}[i,xi]
by A21, A23, A24, XXREAL_0:2; :: thesis: verum

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

r . i <= l9 . i by A16, A17, A18, Th13;

hence S

suppose A25:
l9 . i <= l . i
; :: thesis: ex xi being Element of REAL st S_{1}[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 S_{1}[i,xi]
by A13, A26; :: thesis: verum

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

A27: for i being Element of Seg d holds S

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