:: deftheorem defines \, MMLQUER2:def 3 :
for R1, R2 being Relation holds R1 \, R2 = R1 \/ (R2 \ (R1 ~));