:: deftheorem defines complete LTLAXIO3:def 11 :
for P being PNPair holds
( P is complete iff tau (rng P) = rng P );