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