let p be Rational; :: thesis: p " is Rational
p " = 1 / p ;
hence p " is Rational ; :: thesis: verum