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

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

assume A5: REAL_ratio (a,b) = REAL_ratio (c,d) ; :: thesis: REAL_ratio (b,a) = REAL_ratio (d,c)
1 / (s / r) = r / s by XCMPLX_1:57;
then r / s = r9 / s9 by A5, A1, A2, XCMPLX_1:57;
hence REAL_ratio (b,a) = REAL_ratio (d,c) by A1, A2, A3, Def01; :: thesis: verum

end;

assume A6: REAL_ratio (b,a) = REAL_ratio (d,c) ; :: thesis: REAL_ratio (a,b) = REAL_ratio (c,d)
1 / (s99 / r99) = r99 / s99 by XCMPLX_1:57;
then r99 / s99 = r999 / s999 by A6, A3, A4, XCMPLX_1:57;
hence REAL_ratio (a,b) = REAL_ratio (c,d) by Def01, A2, A4, A3; :: thesis: verum