theorem Th24: :: CHAIN_1:27

for d being non zero Nat
for x being Element of REAL d holds cell (x,x) = {x}