for a, b, c, d being Element of REALPLUS holds
( REAL_ratio (a,b) = REAL_ratio (c,d) iff REAL_ratio (b,a) = REAL_ratio (d,c) )