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

A1: now

assume A2: ( p < 0 & q = 1 / p ) ; :: thesis: ( numerator q = - (denominator p) & denominator q = - (numerator p) )
set r = - p;
A3: 0 < - p by A2, XREAL_1:60;
set s = - q;
- q = 1 / (- p) by A2, XCMPLX_1:189;
then ( numerator (- q) = denominator (- p) & denominator (- q) = numerator (- p) ) by A3, Th88;
then ( - (numerator q) = denominator (- p) & denominator q = numerator (- p) ) by Th87;
then ( - (- (numerator q)) = - (denominator p) & denominator q = - (numerator p) ) by Th87;
hence ( numerator q = - (denominator p) & denominator q = - (numerator p) ) ; :: thesis: verum

end;

now

assume A4: ( numerator q = - (denominator p) & denominator q = - (numerator p) ) ; :: thesis: ( p < 0 & q = 1 / p )
then 0 < - (numerator p) by Th27;
then numerator p < 0 ;
hence p < 0 ; :: thesis: q = 1 / p
thus q = (- (denominator p)) / (- (numerator p)) by A4, Th37
.= - ((denominator p) / (- (numerator p)))
.= - (- ((denominator p) / (numerator p))) by XCMPLX_1:189
.= (1 * (denominator p)) / (numerator p)
.= 1 / ((numerator p) / (denominator p)) by XCMPLX_1:78
.= 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