let w be Element of Inf_seq AtomicFamily; :: thesis: for v being neg-inner-most LTL-formula holds
( w |= v iff w |= * ('X' (init v)) )
let v be neg-inner-most LTL-formula; :: thesis: ( w |= v iff w |= * ('X' (init v)) )
set N = init v;
set M = 'X' (init v);
A1: * ('X' (init v)) = {v} by Lm34;
A2: ( w |= * ('X' (init v)) implies w |= v )

proof

assume A3: w |= * ('X' (init v)) ; :: thesis: w |= v
v in * ('X' (init v)) by A1, TARSKI:def 1;
hence w |= v by A3, MODELC_2:def 64; :: thesis: verum

end;

( w |= v implies w |= * ('X' (init v)) )

proof

assume w |= v ; :: thesis: w |= * ('X' (init v))
then for H being LTL-formula st H in * ('X' (init v)) holds
w |= H by A1, TARSKI:def 1;
hence w |= * ('X' (init v)) by MODELC_2:def 64; :: thesis: verum

end;

hence ( w |= v iff w |= * ('X' (init v)) ) by A2; :: thesis: verum