let a, b, c, d be Element of REALPLUS ; ( 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 ( 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)
;
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;
verum
end;
assume A6:
REAL_ratio (b,a) = REAL_ratio (d,c)
; 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; verum