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

A1: now

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

end;

now

assume that
A7: numerator q = - (denominator p) and
A8: denominator q = - (numerator p) ; :: thesis: ( p < 0 & q = 1 / p )
thus p < 0 by A8, Th27; :: thesis: q = 1 / p
thus q = (- (denominator p)) / (- (numerator p)) by A7, A8, Th37
.= - ((denominator p) / (- (numerator p)))
.= - (- ((denominator p) / (numerator p))) by XCMPLX_1:188
.= (1 * (denominator p)) / (numerator p)
.= 1 / ((numerator p) / (denominator p)) by XCMPLX_1:77
.= 1 / p by Th37 ; :: thesis: verum

end;

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