consider Q being consistent PNPair such that
A1: ( rng (P `1) c= rng (Q `1) & rng (P `2) c= rng (Q `2) & tau (rng P) = rng Q ) by LTLAXIO3:34;
Q is_completion_of P by A1;
then Q in { R where R is consistent PNPair : R is_completion_of P } ;
hence not comp P is empty ; :: thesis: verum