:: deftheorem defines Rrank CLASSES3:def 6 :
for x being object holds Rrank x = Rank (the_rank_of x);