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