theorem Th28: :: CHAIN_1:31

for d being non zero Nat
for l, r, l9, r9 being Element of REAL d st ( for i being Element of Seg d holds l . i <= r . i or for i being Element of Seg d holds l . i > r . i ) holds
( cell (l,r) = cell (l9,r9) iff ( l = l9 & r = r9 ) )