theorem Th1: :: LTLAXIO5:9

for F being Subset of LTLB_WFF
for M being LTLModel st M |= F holds
M |=0 F