:: deftheorem defines in MMLQUERY:def 1 :
for x, y, R being set holds
( x,y in R iff [x,y] in R );