let k be Nat; :: thesis: for d being non zero 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 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 that

A1: k <= d and

A2: 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 ) )

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 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 that

A1: k <= d and

A2: 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, A2, Th30;

end;

( 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, A2, Th30;

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

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

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

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

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