let P be PNPair; :: thesis: ( P = [(<*> LTLB_WFF),(<*> LTLB_WFF)] implies P is complete )
assume A1: P = [(<*> LTLB_WFF),(<*> LTLB_WFF)] ; :: thesis: P is complete
then A2: rng (P `1) = {} ;
rng (P `2) = {} by A1;
then tau (rng P) = rng P by A2;
hence P is complete ; :: thesis: verum