theorem Th23: :: CHAIN_1:26

for d being non zero Nat
for l, r being Element of REAL d holds
( l in cell (l,r) & r in cell (l,r) )