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