let F, G, v be LTL-formula; for q being sequence of (LTLStates v) st F 'U' G in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ex i being Nat st
( i >= 1 & not ( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) & not G in the LTLold of (CastNode ((q . i),v)) ) ) holds
ex j being Nat st
( j >= 1 & G in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) ) ) )
let q be sequence of (LTLStates v); ( F 'U' G in the LTLold of (CastNode ((q . 1),v)) & ( for i being Nat holds CastNode ((q . (i + 1)),v) is_next_of CastNode ((q . i),v) ) & ex i being Nat st
( i >= 1 & not ( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) & not G in the LTLold of (CastNode ((q . i),v)) ) ) implies ex j being Nat st
( j >= 1 & G in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) ) ) ) )
deffunc H1( Nat) -> strict LTLnode over v = CastNode ((q . $1),v);
assume A1:
( F 'U' G in the LTLold of H1(1) & ( for i being Nat holds H1(i + 1) is_next_of H1(i) ) )
; ( for i being Nat st i >= 1 holds
( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) & not G in the LTLold of (CastNode ((q . i),v)) ) or ex j being Nat st
( j >= 1 & G in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) ) ) ) )
( ex i being Nat st
( i >= 1 & not ( F 'U' G in the LTLold of H1(i) & F in the LTLold of H1(i) & not G in the LTLold of H1(i) ) ) implies ex j being Nat st
( j >= 1 & G in the LTLold of H1(j) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of H1(i) & F in the LTLold of H1(i) ) ) ) )
hence
( for i being Nat st i >= 1 holds
( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) & not G in the LTLold of (CastNode ((q . i),v)) ) or ex j being Nat st
( j >= 1 & G in the LTLold of (CastNode ((q . j),v)) & ( for i being Nat st 1 <= i & i < j holds
( F 'U' G in the LTLold of (CastNode ((q . i),v)) & F in the LTLold of (CastNode ((q . i),v)) ) ) ) )
; verum