theorem Th44: :: CHAIN_1:47

for d being non zero Nat
for l, r, l9, r9 being Element of REAL d
for G being Grating of d
for X, X9 being Subset of (Seg d) st cell (l,r) c= cell (l9,r9) & ( 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
( ( i in X9 & l9 . i < r9 . i & [(l9 . i),(r9 . i)] is Gap of G . i ) or ( not i in X9 & l9 . i = r9 . i & l9 . i in G . i ) ) ) holds
( X c= X9 & ( for i being Element of Seg d st ( i in X or not i in X9 ) holds
( l . i = l9 . i & r . i = r9 . i ) ) & ( for i being Element of Seg d st not i in X & i in X9 & not ( l . i = l9 . i & r . i = l9 . i ) holds
( l . i = r9 . i & r . i = r9 . i ) ) )