let k, k9 be Nat; 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; 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; 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; ( 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)
; ( 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)
; 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 = l9 . i0 )
;
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 ) )
;
verum end; suppose
(
l . i0 = r9 . i0 &
r . i0 = r9 . i0 )
;
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 ) )
;
verum end; suppose A12:
r9 . i0 < l9 . i0
;
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 ) )
;
contradictiondefpred 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;
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 A20:
l . i <= r9 . i
;
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
;
S1[i,xi]
r . i <= l9 . i
by A16, A17, A18, Th13;
hence
S1[
i,
xi]
by A21, A23, A24, XXREAL_0:2;
verum end; suppose A25:
l9 . i <= l . i
;
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;
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;
verum end; end;