:: deftheorem defines ^ LTLAXIO4:def 3 :
for F being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds F ^ = { (P ^) where P is Element of [:(LTLB_WFF **),(LTLB_WFF **):] : P in F } ;