:: deftheorem defines comp LTLAXIO4:def 4 :
for F being finite Subset of LTLB_WFF holds comp F = { Q where Q is PNPair : ( rng Q = tau F & rng (Q `1) misses rng (Q `2) ) } ;