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

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

proof

let n be Element of NAT ; :: according to LTLAXIO1:def 12 :: thesis: (SAT (M ^\ i)) . [n,p] = 1
(SAT M) . [(i + n),p] = 1 by A2, A1, Def12;
hence (SAT (M ^\ i)) . [n,p] = 1 by Th28; :: thesis: verum

end;

end;