let y be ExtReal; :: thesis: ( not y " = 0 or y = +infty or y = -infty or y = 0 )
assume A1: y " = 0 ; :: thesis: ( y = +infty or y = -infty or y = 0 )
assume ( y <> +infty & y <> -infty ) ; :: thesis: y = 0
then y in REAL by XXREAL_0:14;
then reconsider y = y as Real ;
(y ") " = 0 by A1;
hence y = 0 ; :: thesis: verum