let d be non zero Nat; :: thesis: for G being Grating of d

for A being Subset of (REAL d) holds

( A in cells (1,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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) )

let G be Grating of d; :: thesis: for A being Subset of (REAL d) holds

( A in cells (1,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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) )

A1: d >= 1 by Def2;

let A be Subset of (REAL d); :: thesis: ( A in cells (1,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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) )

A11: ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) and

A12: [(l . i0),(r . i0)] is Gap of G . i0 and

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

( l . i = r . i & l . i in G . i ) ; :: thesis: A in cells (1,G)

set X = {i0};

for A being Subset of (REAL d) holds

( A in cells (1,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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) )

let G be Grating of d; :: thesis: for A being Subset of (REAL d) holds

( A in cells (1,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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) )

A1: d >= 1 by Def2;

let A be Subset of (REAL d); :: thesis: ( A in cells (1,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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in 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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) implies A in cells (1,G) )

given l, r being Element of REAL d, i0 being Element of Seg d such that A10:
A = cell (l,r)
and ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) implies A in cells (1,G) )

assume
A in cells (1,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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

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

A2: A = cell (l,r) and

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

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

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A1, 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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

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

( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

thus ex i0 being Element of Seg d st

( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) :: thesis: verum

end;( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

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

A2: A = cell (l,r) and

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

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

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A1, 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 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

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

( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

thus ex i0 being Element of Seg d st

( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) ) :: thesis: verum

proof
end;

per cases
( ex X being Subset of (Seg d) st

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

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

end;

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

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

suppose
ex X being Subset of (Seg d) st

( card X = 1 & ( 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 ) ) ) ) ; :: thesis: ex i0 being Element of Seg d st

( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

( card X = 1 & ( 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 ) ) ) ) ; :: thesis: ex i0 being Element of Seg d st

( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

then consider X being Subset of (Seg d) such that

A4: card X = 1 and

A5: 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 ) ) ;

consider i0 being object such that

A6: X = {i0} by A4, CARD_2:42;

A7: i0 in X by A6, TARSKI:def 1;

then reconsider i0 = i0 as Element of Seg d ;

take i0 ; :: thesis: ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

thus ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 ) by A2, A5, A7; :: thesis: for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i = r . i & l . i in G . i ) )

( not i in X iff i <> i0 ) by A6, TARSKI:def 1;

hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A5; :: thesis: verum

end;A4: card X = 1 and

A5: 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 ) ) ;

consider i0 being object such that

A6: X = {i0} by A4, CARD_2:42;

A7: i0 in X by A6, TARSKI:def 1;

then reconsider i0 = i0 as Element of Seg d ;

take i0 ; :: thesis: ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

thus ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 ) by A2, A5, A7; :: thesis: for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i = r . i & l . i in G . i ) )

( not i in X iff i <> i0 ) by A6, TARSKI:def 1;

hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A5; :: thesis: verum

suppose A8:
( d = 1 & ( for i being Element of Seg d holds

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: ex i0 being Element of Seg d st

( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: ex i0 being Element of Seg d st

( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

reconsider i0 = 1 as Element of Seg d by A1, FINSEQ_1:1;

take i0 ; :: thesis: ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

thus ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 ) by A2, A8; :: thesis: for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i = r . i & l . i in G . i ) )

A9: 1 <= i by FINSEQ_1:1;

i <= d by FINSEQ_1:1;

hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A8, A9, XXREAL_0:1; :: thesis: verum

end;take i0 ; :: thesis: ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 & ( for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i ) ) )

thus ( A = cell (l,r) & ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) & [(l . i0),(r . i0)] is Gap of G . i0 ) by A2, A8; :: thesis: for i being Element of Seg d st i <> i0 holds

( l . i = r . i & l . i in G . i )

let i be Element of Seg d; :: thesis: ( i <> i0 implies ( l . i = r . i & l . i in G . i ) )

A9: 1 <= i by FINSEQ_1:1;

i <= d by FINSEQ_1:1;

hence ( i <> i0 implies ( l . i = r . i & l . i in G . i ) ) by A8, A9, XXREAL_0:1; :: thesis: verum

A11: ( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) ) and

A12: [(l . i0),(r . i0)] is Gap of G . i0 and

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

( l . i = r . i & l . i in G . i ) ; :: thesis: A in cells (1,G)

set X = {i0};

per cases
( l . i0 < r . i0 or ( d = 1 & r . i0 < l . i0 ) )
by A11;

end;

suppose A14:
l . i0 < r . i0
; :: thesis: A in cells (1,G)

A15:
card {i0} = 1
by CARD_1:30;

end;now :: thesis: for i being Element of Seg d holds

( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) )

hence
A in cells (1,G)
by A1, A10, A15, Th29; :: thesis: verum( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) )

let i be Element of Seg d; :: thesis: ( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) )

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

hence ( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) ) by A12, A13, A14; :: thesis: verum

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

hence ( ( i in {i0} & l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( not i in {i0} & l . i = r . i & l . i in G . i ) ) by A12, A13, A14; :: thesis: verum

suppose A16:
( d = 1 & r . i0 < l . i0 )
; :: thesis: A in cells (1,G)

end;

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

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

hence
A in cells (1,G)
by A10, A11, Th29; :: thesis: verum( r . i < l . i & [(l . i),(r . i)] is Gap of G . i )

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

A17: 1 <= i by FINSEQ_1:1;

A18: i <= d by FINSEQ_1:1;

A19: 1 <= i0 by FINSEQ_1:1;

A20: i0 <= d by FINSEQ_1:1;

A21: i = 1 by A16, A17, A18, XXREAL_0:1;

i0 = 1 by A16, A19, A20, XXREAL_0:1;

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

end;A17: 1 <= i by FINSEQ_1:1;

A18: i <= d by FINSEQ_1:1;

A19: 1 <= i0 by FINSEQ_1:1;

A20: i0 <= d by FINSEQ_1:1;

A21: i = 1 by A16, A17, A18, XXREAL_0:1;

i0 = 1 by A16, A19, A20, XXREAL_0:1;

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