:: deftheorem defines compn LTLAXIO4:def 10 :
for P being PNPair holds compn P = { Q where Q is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : Q in comp (untn P) } ;