p " = 1 / p ;
hence p " is rational ; :: thesis: verum