for P, Q, R being PNPair st Q in compn P & R in untn P holds
Q is_completion_of R