theorem Th10: :: LTLAXIO4:10

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