:: deftheorem defines |= LTLAXIO1:def 13 :
for M being LTLModel
for F being Subset of LTLB_WFF holds
( M |= F iff for p being Element of LTLB_WFF st p in F holds
M |= p );