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