let d9 be Nat; :: thesis: for d being non zero Nat

for G being Grating of d st d = d9 + 1 holds

for A being Subset of (REAL d) holds

( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

let d be non zero Nat; :: thesis: for G being Grating of d st d = d9 + 1 holds

for A being Subset of (REAL d) holds

( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

let G be Grating of d; :: thesis: ( d = d9 + 1 implies for A being Subset of (REAL d) holds

( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

assume A1: d = d9 + 1 ; :: thesis: for A being Subset of (REAL d) holds

( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

then A2: d9 < d by NAT_1:13;

let A be Subset of (REAL d); :: thesis: ( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

A10: l . i0 = r . i0 and

A11: l . i0 in G . i0 and

A12: for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ; :: thesis: A in cells (d9,G)

reconsider X = (Seg d) \ {i0} as Subset of (Seg d) by XBOOLE_1:36;

( card X = d9 & ( 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 ) ) ) )

for G being Grating of d st d = d9 + 1 holds

for A being Subset of (REAL d) holds

( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

let d be non zero Nat; :: thesis: for G being Grating of d st d = d9 + 1 holds

for A being Subset of (REAL d) holds

( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

let G be Grating of d; :: thesis: ( d = d9 + 1 implies for A being Subset of (REAL d) holds

( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

assume A1: d = d9 + 1 ; :: thesis: for A being Subset of (REAL d) holds

( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

then A2: d9 < d by NAT_1:13;

let A be Subset of (REAL d); :: thesis: ( A in cells (d9,G) iff ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )

hereby :: thesis: ( ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) implies A in cells (d9,G) )

given l, r being Element of REAL d, i0 being Element of Seg d such that A9:
A = cell (l,r)
and ( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) ) implies A in cells (d9,G) )

assume
A in cells (d9,G)
; :: thesis: ex l, r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

then consider l, r being Element of REAL d such that

A3: A = cell (l,r) and

A4: ( ex X being Subset of (Seg d) st

( card X = d9 & ( 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 ) ) ) ) or ( d9 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A2, Th29;

take l = l; :: thesis: ex r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

take r = r; :: thesis: ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

consider X being Subset of (Seg d) such that

A5: card X = d9 and

A6: 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 A1, A4;

card ((Seg d) \ X) = (card (Seg d)) - (card X) by CARD_2:44

.= d - d9 by A5, FINSEQ_1:57

.= 1 by A1 ;

then consider i0 being object such that

A7: (Seg d) \ X = {i0} by CARD_2:42;

i0 in (Seg d) \ X by A7, TARSKI:def 1;

then reconsider i0 = i0 as Element of Seg d by XBOOLE_0:def 5;

take i0 = i0; :: thesis: ( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

not i0 in X by A8;

hence ( l . i0 = r . i0 & l . i0 in G . i0 ) by A6; :: thesis: for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) )

assume i <> i0 ; :: thesis: ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )

then i in X by A8;

hence ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) by A6; :: thesis: verum

end;( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

then consider l, r being Element of REAL d such that

A3: A = cell (l,r) and

A4: ( ex X being Subset of (Seg d) st

( card X = d9 & ( 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 ) ) ) ) or ( d9 = d & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A2, Th29;

take l = l; :: thesis: ex r being Element of REAL d ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

take r = r; :: thesis: ex i0 being Element of Seg d st

( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

consider X being Subset of (Seg d) such that

A5: card X = d9 and

A6: 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 A1, A4;

card ((Seg d) \ X) = (card (Seg d)) - (card X) by CARD_2:44

.= d - d9 by A5, FINSEQ_1:57

.= 1 by A1 ;

then consider i0 being object such that

A7: (Seg d) \ X = {i0} by CARD_2:42;

i0 in (Seg d) \ X by A7, TARSKI:def 1;

then reconsider i0 = i0 as Element of Seg d by XBOOLE_0:def 5;

take i0 = i0; :: thesis: ( A = cell (l,r) & l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

A8: now :: thesis: for i being Element of Seg d holds

( i in X iff i <> i0 )

thus
A = cell (l,r)
by A3; :: thesis: ( l . i0 = r . i0 & l . i0 in G . i0 & ( for i being Element of Seg d st i <> i0 holds ( i in X iff i <> i0 )

let i be Element of Seg d; :: thesis: ( i in X iff i <> i0 )

( i in (Seg d) \ X iff i = i0 ) by A7, TARSKI:def 1;

hence ( i in X iff i <> i0 ) by XBOOLE_0:def 5; :: thesis: verum

end;( i in (Seg d) \ X iff i = i0 ) by A7, TARSKI:def 1;

hence ( i in X iff i <> i0 ) by XBOOLE_0:def 5; :: thesis: verum

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ) )

not i0 in X by A8;

hence ( l . i0 = r . i0 & l . i0 in G . i0 ) by A6; :: thesis: for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) )

assume i <> i0 ; :: thesis: ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i )

then i in X by A8;

hence ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) by A6; :: thesis: verum

A10: l . i0 = r . i0 and

A11: l . i0 in G . i0 and

A12: for i being Element of Seg d st i <> i0 holds

( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) ; :: thesis: A in cells (d9,G)

reconsider X = (Seg d) \ {i0} as Subset of (Seg d) by XBOOLE_1:36;

( card X = d9 & ( 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 ) ) ) )

proof

hence
A in cells (d9,G)
by A2, A9, Th29; :: thesis: verum
thus card X =
(card (Seg d)) - (card {i0})
by CARD_2:44

.= d - (card {i0}) by FINSEQ_1:57

.= d - 1 by CARD_1:30

.= d9 by A1 ; :: thesis: 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 ) )

let i be Element of Seg d; :: thesis: ( ( 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 ) )

( i in {i0} iff i = i0 ) by TARSKI:def 1;

hence ( ( 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 A10, A11, A12, XBOOLE_0:def 5; :: thesis: verum

end;.= d - (card {i0}) by FINSEQ_1:57

.= d - 1 by CARD_1:30

.= d9 by A1 ; :: thesis: 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 ) )

let i be Element of Seg d; :: thesis: ( ( 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 ) )

( i in {i0} iff i = i0 ) by TARSKI:def 1;

hence ( ( 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 A10, A11, A12, XBOOLE_0:def 5; :: thesis: verum