theorem Th3: :: MESFUNC5:3

for x, y being R_eal
for e being Real holds
( not |.(x - y).| < e or ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x <> +infty & x <> -infty & y <> +infty & y <> -infty ) )