let a be positive Rational; :: thesis: ( numerator a = denominator (a ") & denominator a = numerator (a ") )
a " = 1 / a ;
hence ( numerator a = denominator (a ") & denominator a = numerator (a ") ) by RAT_1:44; :: thesis: verum