let P, Q be PNPair; :: thesis: ( Q in compn P implies Q is complete )
assume A1: Q in compn P ; :: thesis: Q is complete
then consider Q1 being PNPair such that
Q1 = Q and
A2: Q1 in comp (untn P) ;
consider x being set such that
Q1 in x and
A3: x in { (comp R) where R is PNPair : R in untn P } by A2, TARSKI:def 4;
ex R being PNPair st
( x = comp R & R in untn P ) by A3;
hence Q is complete by Th19, A1, Th13; :: thesis: verum