theorem Th11: :: EXTREAL1:22

for x, y being ExtReal st - y < x & x < y holds
( 0 < y & |.x.| < y )