let a be rational number ; :: thesis: for b being real irrational number st a <> 0 holds
a / b is irrational
let b be real irrational number ; :: thesis: ( a <> 0 implies a / b is irrational )
assume A1: a <> 0 ; :: thesis: a / b is irrational
assume not a / b is irrational ; :: thesis: contradiction
then reconsider c = a / b as rational number ;
c * b is irrational by A1, Th42, XCMPLX_1:50;
hence contradiction by XCMPLX_1:88; :: thesis: verum