theorem Th19: :: REVROT_1:19

for n being non zero Nat holds 0.REAL n <> 1.REAL n