theorem Th19: :: LTLAXIO4:19

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