theorem Th13: :: LTLAXIO4:13

for P, Q being PNPair st Q is_completion_of P holds
Q is complete by LTLAXIO3:17;