let x be Element of comp F; :: thesis: x is complete
x in comp F ;
then ex Q being PNPair st
( Q = x & rng Q = tau F & rng (Q `1) misses rng (Q `2) ) ;
then tau (rng x) = rng x by LTLAXIO3:17;
hence x is complete ; :: thesis: verum