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