let x, y be R_eal; :: thesis: 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 ) )
let e be Real; :: thesis: ( not |.(x - y).| < e or ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x <> +infty & x <> -infty & y <> +infty & y <> -infty ) )
assume A1: |.(x - y).| < e ; :: thesis: ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x <> +infty & x <> -infty & y <> +infty & y <> -infty ) )
y - x <= |.(x - y).| by Th2;
then A2: y - x < e by A1, XXREAL_0:2;
x - y <= |.(x - y).| by EXTREAL1:20;
then x - y < e by A1, XXREAL_0:2;
hence ( ( x = +infty & y = +infty ) or ( x = -infty & y = -infty ) or ( x <> +infty & x <> -infty & y <> +infty & y <> -infty ) ) by A2, XXREAL_3:54; :: thesis: verum