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

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 ( 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, Th34;

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

then consider X being Subset of (Seg d) such that
A2: ( 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 ) ) ) ) ;
thus ( for i being Element of Seg d holds
( ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( 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; :: thesis: verum

end;

suppose ( k = d & ( for i being Element of Seg d holds
( r . i < l . i & [(l . i),(r . i)] is Gap of G . i ) ) ) ; :: thesis: ( for i being Element of Seg d holds
( ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( 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 ) )

hence ( for i being Element of Seg d holds
( ( l . i < r . i & [(l . i),(r . i)] is Gap of G . i ) or ( 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 ) ) ; :: thesis: verum

end;

end;