let p be Rational; :: thesis: for w being Nat holds

( not 1 < w or for m being Integer

for k being Nat holds

( not numerator p = m * w or not denominator p = k * w ) )

assume ex w being Nat st

( 1 < w & ex m being Integer ex k being Nat st

( numerator p = m * w & denominator p = k * w ) ) ; :: thesis: contradiction

then consider w being Nat such that

A1: 1 < w and

A2: ex m being Integer ex k being Nat st

( numerator p = m * w & denominator p = k * w ) ;

consider m being Integer, k being Nat such that

A3: numerator p = m * w and

A4: denominator p = k * w by A2;

A5: p = (m * w) / (k * w) by A3, A4, Th12

.= (m / k) * (w / w) by XCMPLX_1:76

.= (m / k) * 1 by A1, XCMPLX_1:60

.= m / k ;

A6: k <> 0 by A4;

then k * 1 < k * w by A1, XREAL_1:68;

hence contradiction by A4, A6, A5, Def3; :: thesis: verum

( not 1 < w or for m being Integer

for k being Nat holds

( not numerator p = m * w or not denominator p = k * w ) )

assume ex w being Nat st

( 1 < w & ex m being Integer ex k being Nat st

( numerator p = m * w & denominator p = k * w ) ) ; :: thesis: contradiction

then consider w being Nat such that

A1: 1 < w and

A2: ex m being Integer ex k being Nat st

( numerator p = m * w & denominator p = k * w ) ;

consider m being Integer, k being Nat such that

A3: numerator p = m * w and

A4: denominator p = k * w by A2;

A5: p = (m * w) / (k * w) by A3, A4, Th12

.= (m / k) * (w / w) by XCMPLX_1:76

.= (m / k) * 1 by A1, XCMPLX_1:60

.= m / k ;

A6: k <> 0 by A4;

then k * 1 < k * w by A1, XREAL_1:68;

hence contradiction by A4, A6, A5, Def3; :: thesis: verum