let d be non zero Element of 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 l', r' being Element of REAL d, i0 being Element of Seg d such that
A1: cell l,r = cell l',r' and
A2: ( l' . i0 < r' . i0 or ( d = 1 & r' . i0 < l' . i0 ) ) and
A3: [(l' . i0),(r' . i0)] is Gap of G . i0 and
A4: for i being Element of Seg d st i <> i0 holds
( l' . i = r' . i & l' . i in G . i ) by Th44;
A5: ( for i being Element of Seg d holds l' . i <= r' . i or for i being Element of Seg d holds r' . i < l' . i )

proof

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

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

now

let i be Element of Seg d; :: thesis: l' . i <= r' . i
( i = i0 or i <> i0 ) ;
hence l' . i <= r' . i by A4, A6; :: thesis: verum

end;

hence ( for i being Element of Seg d holds l' . i <= r' . i or for i being Element of Seg d holds r' . i < l' . i ) ; :: thesis: verum

end;

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

now

let i be Element of Seg d; :: thesis: r' . i < l' . i
A8: 1 <= i by FINSEQ_1:3;
A9: i <= d by FINSEQ_1:3;
A10: 1 <= i0 by FINSEQ_1:3;
A11: i0 <= d by FINSEQ_1:3;
A12: i = 1 by A7, A8, A9, XXREAL_0:1;
i0 = 1 by A7, A10, A11, XXREAL_0:1;
hence r' . i < l' . i by A7, A12; :: thesis: verum

end;

hence ( for i being Element of Seg d holds l' . i <= r' . i or for i being Element of Seg d holds r' . i < l' . i ) ; :: thesis: verum

end;

end;

end;

then A13: l = l' by A1, Th32;
r = r' by A1, A5, Th32;
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 Th44; :: thesis: verum