let p be Rational; :: thesis: ( ( numerator p = p or denominator p = 1 ) & 0 <= p implies p is Element of NAT )

assume that

A1: ( numerator p = p or denominator p = 1 ) and

A2: 0 <= p ; :: thesis: p is Element of NAT

p is Integer by A1, Th15;

hence p is Element of NAT by A2, INT_1:3; :: thesis: verum

assume that

A1: ( numerator p = p or denominator p = 1 ) and

A2: 0 <= p ; :: thesis: p is Element of NAT

p is Integer by A1, Th15;

hence p is Element of NAT by A2, INT_1:3; :: thesis: verum