set p = 1 / 2;
assume 1 / 2 is integer ; :: thesis: contradiction
then A1: ( denominator (1 / 2) = 1 & numerator (1 / 2) = 1 / 2 ) by Th14;
A2: numerator (1 / (1 / 2)) = denominator (1 / 2) by Th41;
denominator (1 / 2) = 2 by A2, Th14;
hence contradiction by A1; :: thesis: verum