:: deftheorem Def5 defines <=' ARYTM_2:def 5 :
for x, y being Element of REAL+ holds
( ( x in RAT+ & y in RAT+ implies ( x <=' y iff ex x9, y9 being Element of RAT+ st
( x = x9 & y = y9 & x9 <=' y9 ) ) ) & ( x in RAT+ & not y in RAT+ implies ( x <=' y iff x in y ) ) & ( not x in RAT+ & y in RAT+ implies ( x <=' y iff not y in x ) ) & ( ( not x in RAT+ or not y in RAT+ ) & ( not x in RAT+ or y in RAT+ ) & ( x in RAT+ or not y in RAT+ ) implies ( x <=' y iff x c= y ) ) );