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