defpred S₁[ PNPair] means $1 in comp (untn P);
deffunc H₃( PNPair) -> PNPair = $1;
A1: comp (untn P) is finite ;
A2: { H₃(Q) where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } is finite from FRAENKEL:sch 21(A1);
{ Q where Q is PNPair : S₁[Q] } c= [:(LTLB_WFF **),(LTLB_WFF **):] from FRAENKEL:sch 10();
hence { Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] by A2; :: thesis: verum