:: deftheorem defines +*2 FOMODEL0:def 30 :
for P, Q being Relation holds P +*2 Q = (P | ((dom P) \ (dom Q))) \/ Q;