for F being Subset of LTLB_WFF
for i being Element of NAT
for M being LTLModel st M |= F holds
M ^\ i |= F