theorem th263: :: LTLAXIO5:21

for A, B being Element of LTLB_WFF
for F being Subset of LTLB_WFF holds
( F \/ {A} |=0 B iff F |=0 A => B )