:: deftheorem defines comp LTLAXIO4:def 7 :
for X being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds comp X = union { (comp P) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in X } ;