:: deftheorem defines |=0 LTLAXIO5:def 2 :
for M being LTLModel
for F being Subset of LTLB_WFF holds
( M |=0 F iff for A being Element of LTLB_WFF st A in F holds
M |=0 A );