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

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;

end;

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;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