:: deftheorem defines +*1 FOMODEL0:def 29 :
for P, Q being Relation holds P +*1 Q = (P \ [:(dom Q),(rng P):]) \/ Q;