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