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

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

set s = - (1 / p);
set r = - p;
assume A2: p < 0 ; :: thesis: ( numerator (1 / p) = - (denominator p) & denominator (1 / p) = - (numerator p) )
A4: - (1 / p) = 1 / (- p) by XCMPLX_1:188;
A5: 0 < - p by A2, XREAL_1:58;
then numerator (- (1 / p)) = denominator (- p) by A4, Th41;
then - (numerator (1 / p)) = denominator (- p) by Th40;
then A6: - (- (numerator (1 / p))) = - (denominator p) by Th40;
denominator (- (1 / p)) = numerator (- p) by A5, A4, Th41;
then denominator (1 / p) = numerator (- p) by Th40;
hence ( numerator (1 / p) = - (denominator p) & denominator (1 / p) = - (numerator p) ) by A6, Th40; :: thesis: verum

end;

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