let F be Subset of LTLB_WFF; :: thesis: for i being Element of NAT

for M being LTLModel st M |= F holds

M ^\ i |= F

let i be Element of NAT ; :: thesis: for M being LTLModel st M |= F holds

M ^\ i |= F

let M be LTLModel; :: thesis: ( M |= F implies M ^\ i |= F )

assume A1: M |= F ; :: thesis: M ^\ i |= F

thus M ^\ i |= F :: thesis: verum

for M being LTLModel st M |= F holds

M ^\ i |= F

let i be Element of NAT ; :: thesis: for M being LTLModel st M |= F holds

M ^\ i |= F

let M be LTLModel; :: thesis: ( M |= F implies M ^\ i |= F )

assume A1: M |= F ; :: thesis: M ^\ i |= F

thus M ^\ i |= F :: thesis: verum

proof

let p be Element of LTLB_WFF ; :: according to LTLAXIO1:def 13 :: thesis: ( p in F implies M ^\ i |= p )

assume A2: p in F ; :: thesis: M ^\ i |= p

thus M ^\ i |= p :: thesis: verum

end;assume A2: p in F ; :: thesis: M ^\ i |= p

thus M ^\ i |= p :: thesis: verum