let x, y be ExtReal; :: thesis: ( y <> +infty & 0 < x & 0 < y implies 0 < x / y )
assume that
A1: y <> +infty and
A2: 0 < x and
A3: 0 < y ; :: thesis: 0 < x / y
per cases ( x in REAL or x = +infty or x = -infty ) by XXREAL_0:14;
suppose x in REAL ; :: thesis: 0 < x / y
then reconsider x1 = x as Element of REAL ;
reconsider y1 = y as Element of REAL by A1, A3, XXREAL_0:14;
x / y = x1 / y1 ;
hence 0 < x / y by A2, A3; :: thesis: verum
end;
suppose x = +infty ; :: thesis: 0 < x / y
hence 0 < x / y by A1, A3, XXREAL_3:83; :: thesis: verum
end;
suppose x = -infty ; :: thesis: 0 < x / y
hence 0 < x / y by A2; :: thesis: verum
end;
end;