let k be Element of NAT ; :: thesis: for d being non zero Element of NAT
for l, r being Element of REAL d
for G being Grating of d st k <= d holds
( cell l,r in cells k,G iff ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )
let d be non zero Element of NAT ; :: thesis: for l, r being Element of REAL d
for G being Grating of d st k <= d holds
( cell l,r in cells k,G iff ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )
let l, r be Element of REAL d; :: thesis: for G being Grating of d st k <= d holds
( cell l,r in cells k,G iff ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )
let G be Grating of d; :: thesis: ( k <= d implies ( cell l,r in cells k,G iff ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) ) )
assume A1: k <= d ; :: thesis: ( cell l,r in cells k,G iff ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) )

hereby :: thesis: ( ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) implies cell l,r in cells k,G )

assume cell l,r in cells k,G ; :: thesis: ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) )
then consider l', r' being Element of REAL d such that
A2: ( cell l,r = cell l',r' & ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r' . i < l' . i & [(l' . i),(r' . i)] is Gap of G . i ) ) ) ) ) by A1, Th33;
( l = l' & r = r' )

proof

per cases ( ex X being Subset of (Seg d) st
( card X = k & ( 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 for i being Element of Seg d holds
( r' . i < l' . i & [(l' . i),(r' . i)] is Gap of G . i ) ) by A2;

suppose ex X being Subset of (Seg d) st
( card X = k & ( 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: ( l = l' & r = r' )

then consider X being Subset of (Seg d) such that
A3: ( card X = k & ( 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 i being Element of Seg d holds l' . i <= r' . i by A3;
hence ( l = l' & r = r' ) by A2, Th32; :: thesis: verum

end;

suppose for i being Element of Seg d holds
( r' . i < l' . i & [(l' . i),(r' . i)] is Gap of G . i ) ; :: thesis: ( l = l' & r = r' )

hence ( l = l' & r = r' ) by A2, Th32; :: thesis: verum

end;

end;

end;

hence ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) by A2; :: thesis: verum

end;

thus ( ( ex X being Subset of (Seg d) st
( card X = k & ( 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 ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ) implies cell l,r in cells k,G ) by A1, Th33; :: thesis: verum