theorem Th22: :: LTLAXIO1:22

for F, G being Subset of LTLB_WFF
for M being LTLModel holds
( ( M |= F & M |= G ) iff M |= F \/ G )