theorem Th4: :: MODELC_3:4

for L being FinSequence
for H being LTL-formula holds len (L,({} H)) = 0