set c = { Q where Q is consistent PNPair : Q is_completion_of P } ;
set F = tau (rng P);
A1: { Q where Q is consistent PNPair : Q is_completion_of P } c= [:((tau (rng P)) **),((tau (rng P)) **):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { Q where Q is consistent PNPair : Q is_completion_of P } or x in [:((tau (rng P)) **),((tau (rng P)) **):] )
assume x in { Q where Q is consistent PNPair : Q is_completion_of P } ; :: thesis: x in [:((tau (rng P)) **),((tau (rng P)) **):]
then consider Q being consistent PNPair such that
A2: x = Q and
A3: Q is_completion_of P ;
consider y, z being object such that
A4: ( y in LTLB_WFF ** & z in LTLB_WFF ** ) and
A5: Q = [y,z] by ZFMISC_1:def 2;
reconsider y = y, z = z as one-to-one FinSequence of LTLB_WFF by A4, LTLAXIO3:def 2;
A6: tau (rng P) = rng Q by A3
.= (rng y) \/ (rng z) by A5 ;
then z is one-to-one FinSequence of tau (rng P) by XBOOLE_1:7, FINSEQ_1:def 4;
then A7: z in (tau (rng P)) ** by LTLAXIO3:def 2;
y is one-to-one FinSequence of tau (rng P) by A6, XBOOLE_1:7, FINSEQ_1:def 4;
then y in (tau (rng P)) ** by LTLAXIO3:def 2;
hence x in [:((tau (rng P)) **),((tau (rng P)) **):] by A7, ZFMISC_1:def 2, A5, A2; :: thesis: verum

end;

{ Q where Q is consistent PNPair : Q is_completion_of P } c= [:(LTLB_WFF **),(LTLB_WFF **):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { Q where Q is consistent PNPair : Q is_completion_of P } or x in [:(LTLB_WFF **),(LTLB_WFF **):] )
assume x in { Q where Q is consistent PNPair : Q is_completion_of P } ; :: thesis: x in [:(LTLB_WFF **),(LTLB_WFF **):]
then ex Q being consistent PNPair st
( x = Q & Q is_completion_of P ) ;
hence x in [:(LTLB_WFF **),(LTLB_WFF **):] ; :: thesis: verum

end;

hence { Q where Q is consistent PNPair : Q is_completion_of P } is finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] by A1; :: thesis: verum