:: deftheorem defines @ MMLQUERY:def 27 :
for X being set
for S being Subset of X
for R being Relation of X,S holds @ R = R;