:: deftheorem defines is_completion_of LTLAXIO4:def 5 :
for P, Q being PNPair holds
( Q is_completion_of P iff ( rng (P `1) c= rng (Q `1) & rng (P `2) c= rng (Q `2) & tau (rng P) = rng Q ) );