let a, b, c, d be Element of RATPLUS ; :: thesis: ( RAT_ratio (a,b) = RAT_ratio (c,d) iff RAT_ratio (b,a) = RAT_ratio (d,c) )
consider r, s being positive Rational such that
A1: ( a = r & b = s & RAT_ratio (a,b) = s / r ) by Def04;
consider r9, s9 being positive Rational such that
A2: ( c = r9 & d = s9 & RAT_ratio (c,d) = s9 / r9 ) by Def04;
consider r99, s99 being positive Rational such that
A3: ( b = r99 & a = s99 & RAT_ratio (b,a) = s99 / r99 ) by Def04;
consider r999, s999 being positive Rational such that
A4: ( d = r999 & c = s999 & RAT_ratio (d,c) = s999 / r999 ) by Def04;

hereby :: thesis: ( RAT_ratio (b,a) = RAT_ratio (d,c) implies RAT_ratio (a,b) = RAT_ratio (c,d) )

assume A5: RAT_ratio (a,b) = RAT_ratio (c,d) ; :: thesis: RAT_ratio (b,a) = RAT_ratio (d,c)
1 / (s / r) = r / s by XCMPLX_1:57;
hence RAT_ratio (b,a) = RAT_ratio (d,c) by A1, A2, A3, A4, A5, XCMPLX_1:57; :: thesis: verum

end;

assume A6: RAT_ratio (b,a) = RAT_ratio (d,c) ; :: thesis: RAT_ratio (a,b) = RAT_ratio (c,d)
1 / (s99 / r99) = r99 / s99 by XCMPLX_1:57;
hence RAT_ratio (a,b) = RAT_ratio (c,d) by A1, A2, A3, A4, A6, XCMPLX_1:57; :: thesis: verum