for F, G being Subset of [:(LTLB_WFF **),(LTLB_WFF **):] holds (F \/ G) ^ = (F ^) \/ (G ^)