set c = { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;
set tf = tau F;
set f = the Enumeration of tau F;
set x = [ the Enumeration of tau F,(<*> LTLB_WFF)];
A1: { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } c= [:((tau F) **),((tau F) **):]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } or x in [:((tau F) **),((tau F) **):] )
assume x in { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ; :: thesis: x in [:((tau F) **),((tau F) **):]
then consider Q being PNPair such that
A2: x = Q and
A3: rng Q = tau F and
rng (Q `1) misses rng (Q `2) ;
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;
rng y = rng (Q `1) by A5;
then reconsider y = y as one-to-one FinSequence of tau F by XBOOLE_1:7, A3, FINSEQ_1:def 4;
rng z = rng (Q `2) by A5;
then reconsider z = z as one-to-one FinSequence of tau F by XBOOLE_1:7, A3, FINSEQ_1:def 4;
( y in (tau F) ** & z in (tau F) ** ) by LTLAXIO3:def 2;
hence x in [:((tau F) **),((tau F) **):] by ZFMISC_1:def 2, A5, A2; :: thesis: verum

end;

rng ([ the Enumeration of tau F,(<*> LTLB_WFF)] `2) = {} ;
then A6: rng ([ the Enumeration of tau F,(<*> LTLB_WFF)] `1) misses rng ([ the Enumeration of tau F,(<*> LTLB_WFF)] `2) ;
rng [ the Enumeration of tau F,(<*> LTLB_WFF)] = (tau F) \/ (rng (<*> LTLB_WFF)) by RLAFFIN3:def 1
.= tau F ;
then [ the Enumeration of tau F,(<*> LTLB_WFF)] in { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } by A6;
hence { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } is non empty finite Subset of [:(LTLB_WFF **),(LTLB_WFF **):] by A1, XBOOLE_1:1; :: thesis: verum