theorem Th4: :: EXTREAL1:15

for x being ExtReal st x <> 0 holds
0 < |.x.|