let d be non zero Nat; :: thesis: for l, r being Element of REAL d

for G being Grating of d holds

( cell (l,r) in cells (1,G) iff ex i0 being Element of Seg d st

( ( 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 l, r be Element of REAL d; :: thesis: for G being Grating of d holds

( cell (l,r) in cells (1,G) iff ex i0 being Element of Seg d st

( ( 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: ( cell (l,r) in cells (1,G) iff ex i0 being Element of Seg d st

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

( ( 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 cell (l,r) in cells (1,G) ) by Th40; :: thesis: verum

for G being Grating of d holds

( cell (l,r) in cells (1,G) iff ex i0 being Element of Seg d st

( ( 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 l, r be Element of REAL d; :: thesis: for G being Grating of d holds

( cell (l,r) in cells (1,G) iff ex i0 being Element of Seg d st

( ( 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: ( cell (l,r) in cells (1,G) iff ex i0 being Element of Seg d st

( ( 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 i0 being Element of Seg d st

( ( 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 cell (l,r) in cells (1,G) )

thus
( ex i0 being Element of Seg d st ( ( 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 cell (l,r) in cells (1,G) )

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

( ( 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 l9, r9 being Element of REAL d, i0 being Element of Seg d such that

A1: cell (l,r) = cell (l9,r9) and

A2: ( l9 . i0 < r9 . i0 or ( d = 1 & r9 . i0 < l9 . i0 ) ) and

A3: [(l9 . i0),(r9 . i0)] is Gap of G . i0 and

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

( l9 . i = r9 . i & l9 . i in G . i ) by Th40;

A5: ( for i being Element of Seg d holds l9 . i <= r9 . i or for i being Element of Seg d holds r9 . i < l9 . i )

r = r9 by A1, A5, Th28;

hence ex i0 being Element of Seg d st

( ( 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 ) ) ) by A2, A3, A4, A13; :: thesis: verum

end;( ( 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 l9, r9 being Element of REAL d, i0 being Element of Seg d such that

A1: cell (l,r) = cell (l9,r9) and

A2: ( l9 . i0 < r9 . i0 or ( d = 1 & r9 . i0 < l9 . i0 ) ) and

A3: [(l9 . i0),(r9 . i0)] is Gap of G . i0 and

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

( l9 . i = r9 . i & l9 . i in G . i ) by Th40;

A5: ( for i being Element of Seg d holds l9 . i <= r9 . i or for i being Element of Seg d holds r9 . i < l9 . i )

proof
end;

then A13:
l = l9
by A1, Th28;per cases
( l9 . i0 < r9 . i0 or ( d = 1 & r9 . i0 < l9 . i0 ) )
by A2;

end;

suppose A6:
l9 . i0 < r9 . i0
; :: thesis: ( for i being Element of Seg d holds l9 . i <= r9 . i or for i being Element of Seg d holds r9 . i < l9 . i )

end;

now :: thesis: for i being Element of Seg d holds l9 . i <= r9 . i

hence
( for i being Element of Seg d holds l9 . i <= r9 . i or for i being Element of Seg d holds r9 . i < l9 . i )
; :: thesis: verumlet i be Element of Seg d; :: thesis: l9 . i <= r9 . i

( i = i0 or i <> i0 ) ;

hence l9 . i <= r9 . i by A4, A6; :: thesis: verum

end;( i = i0 or i <> i0 ) ;

hence l9 . i <= r9 . i by A4, A6; :: thesis: verum

suppose A7:
( d = 1 & r9 . i0 < l9 . i0 )
; :: thesis: ( for i being Element of Seg d holds l9 . i <= r9 . i or for i being Element of Seg d holds r9 . i < l9 . i )

end;

now :: thesis: for i being Element of Seg d holds r9 . i < l9 . i

hence
( for i being Element of Seg d holds l9 . i <= r9 . i or for i being Element of Seg d holds r9 . i < l9 . i )
; :: thesis: verumlet i be Element of Seg d; :: thesis: r9 . i < l9 . i

A8: 1 <= i by FINSEQ_1:1;

A9: i <= d by FINSEQ_1:1;

A10: 1 <= i0 by FINSEQ_1:1;

A11: i0 <= d by FINSEQ_1:1;

A12: i = 1 by A7, A8, A9, XXREAL_0:1;

i0 = 1 by A7, A10, A11, XXREAL_0:1;

hence r9 . i < l9 . i by A7, A12; :: thesis: verum

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

A9: i <= d by FINSEQ_1:1;

A10: 1 <= i0 by FINSEQ_1:1;

A11: i0 <= d by FINSEQ_1:1;

A12: i = 1 by A7, A8, A9, XXREAL_0:1;

i0 = 1 by A7, A10, A11, XXREAL_0:1;

hence r9 . i < l9 . i by A7, A12; :: thesis: verum

r = r9 by A1, A5, Th28;

hence ex i0 being Element of Seg d st

( ( 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 ) ) ) by A2, A3, A4, A13; :: thesis: verum

( ( 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 cell (l,r) in cells (1,G) ) by Th40; :: thesis: verum