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