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