let a be real number ; :: thesis: ( a is irrational implies not a is zero )
assume A1: a is irrational ; :: thesis: not a is zero
assume a is zero ; :: thesis: contradiction
then a = 0 / 1 ;
hence contradiction by A1; :: thesis: verum