let p be Rational; :: thesis: for l being Element of NAT holds
( not 1 < l or for m being Integer
for k being Element of NAT holds
( not numerator p = m * l or not denominator p = k * l ) )
assume ex l being Element of NAT st
( 1 < l & ex m being Integer ex k being Element of NAT st
( numerator p = m * l & denominator p = k * l ) ) ; :: thesis: contradiction
then consider l being Element of NAT such that
A1: ( 1 < l & ex m being Integer ex k being Element of NAT st
( numerator p = m * l & denominator p = k * l ) ) ;
consider m being Integer, k being Element of NAT such that
A2: ( numerator p = m * l & denominator p = k * l ) by A1;
A3: k <> 0 by A2, Def3;

A4: now

k * 1 < k * l by A1, A3, XREAL_1:70;
hence k < denominator p by A2; :: thesis: verum

end;

p = (m * l) / (k * l) by A2, Th37
.= (m / k) * (l / l) by XCMPLX_1:77
.= (m / k) * 1 by A1, XCMPLX_1:60
.= m / k ;
hence contradiction by A3, A4, Def3; :: thesis: verum