let x, y be ExtReal; :: thesis: ( y <> -infty & y <> +infty & x <> 0 & y <> 0 implies x / y <> 0 )
assume that
A1: ( y <> -infty & y <> +infty ) and
A2: x <> 0 and
A3: y <> 0 ; :: thesis: x / y <> 0
assume x / y = 0 ; :: thesis: contradiction
then y " = 0 by A2;
hence contradiction by A1, A3, XXREAL_3:82; :: thesis: verum