( fp in LTLB_WFF ** & fm in LTLB_WFF ** ) by Def2;
hence [fp,fm] is PNPair by ZFMISC_1:def 2; :: thesis: verum