let p be Rational; :: thesis: ( ( numerator p = p or denominator p = 1 ) implies p is Integer )
assume A1: ( numerator p = p or denominator p = 1 ) ; :: thesis: p is Integer

per cases ( numerator p = p or denominator p = 1 ) by A1;

suppose numerator p = p ; :: thesis: p is Integer

hence p is Integer ; :: thesis: verum

end;

suppose denominator p = 1 ; :: thesis: p is Integer

then numerator p = p ;
hence p is Integer ; :: thesis: verum

end;

end;