consider x being object such that
A1: x in untn P by XBOOLE_0:def 1;
reconsider x = x as consistent PNPair by A1;
consider y being object such that
A2: y in comp x by XBOOLE_0:def 1;
reconsider y = y as PNPair by A2;
comp x in { (comp Q) where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in untn P } by A1;
then y in comp (untn P) by A2, TARSKI:def 4;
then y in { Q where Q is PNPair : Q in comp (untn P) } ;
hence not compn P is empty ; :: thesis: verum