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

assume A1: ( numerator p = p or denominator p = 1 ) ; :: thesis: p is Integer

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

end;