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 ) ) ) )
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) )
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 )
proof
per cases ( l9 . i0 < r9 . i0 or ( d = 1 & r9 . i0 < l9 . i0 ) ) by A2;
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 )
now :: thesis: for i being Element of Seg d holds l9 . i <= r9 . i
let 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;
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: verum
end;
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 )
now :: thesis: for i being Element of Seg d holds r9 . i < l9 . i
let 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;
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: verum
end;
end;
end;
then A13: l = l9 by A1, Th28;
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;
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) ) by Th40; :: thesis: verum