theorem Th20: :: LTLAXIO4:20

for P, Q being PNPair st Q in compn P holds
Q is complete