theorem Th62: :: LTLAXIO2:62

for p, q being Element of LTLB_WFF
for X being Subset of LTLB_WFF holds X |- ('X' (p 'or' q)) => (('X' p) 'or' ('X' q))