:: deftheorem defines rational RAT_1:def 2 :
for r being object holds
( r is rational iff r in RAT );