theorem th262a: :: LTLAXIO5:11

for A being Element of LTLB_WFF
for F being Subset of LTLB_WFF st F |=0 A holds
F |= A