let p be Rational; :: thesis: ( 0 < p iff ( numerator (1 / p) = denominator p & denominator (1 / p) = numerator p ) )
set q = 1 / p;

A1: now :: thesis: ( 0 < p implies ( numerator p = denominator (1 / p) & denominator p = numerator (1 / p) ) )

set x = denominator p;
assume A2: 0 < p ; :: thesis: ( numerator p = denominator (1 / p) & denominator p = numerator (1 / p) )
A4: 1 / p = 1 / ((numerator p) / (denominator p)) by Th12
.= (1 * (denominator p)) / (numerator p) by XCMPLX_1:77
.= (denominator p) / (numerator p) ;
reconsider y = numerator p as Element of NAT by A2, INT_1:3;
A5: for k being Nat holds
( not 1 < k or for m being Integer
for w being Nat holds
( not denominator p = m * k or not y = w * k ) )

proof

assume ex k being Nat st
( 1 < k & ex m being Integer ex w being Nat st
( denominator p = m * k & y = w * k ) ) ; :: thesis: contradiction
then consider k being Nat such that
A6: 1 < k and
A7: ex m being Integer ex w being Nat st
( denominator p = m * k & y = w * k ) ;
consider m being Integer, w being Nat such that
A8: denominator p = m * k and
A9: y = w * k by A7;
0 <= m by A8;
then reconsider z = m as Element of NAT by INT_1:3;
denominator p = z * k by A8;
hence contradiction by A6, A9, Th26; :: thesis: verum

end;

0 <> numerator p by A2, Th35;
hence ( numerator p = denominator (1 / p) & denominator p = numerator (1 / p) ) by A4, A5, Th27; :: thesis: verum

end;

thus ( 0 < p iff ( numerator (1 / p) = denominator p & denominator (1 / p) = numerator p ) ) by A1; :: thesis: verum