let H, v be LTL-formula; :: thesis: for s0, s1, s2 being strict elementary LTLnode over v st s1 is_next_of s0 & s2 is_next_of s1 & H in the LTLold of s1 & H is Until & not the_right_argument_of H in the LTLold of s1 holds
( the_left_argument_of H in the LTLold of s1 & H in the LTLold of s2 )
let s0, s1, s2 be strict elementary LTLnode over v; :: thesis: ( s1 is_next_of s0 & s2 is_next_of s1 & H in the LTLold of s1 & H is Until & not the_right_argument_of H in the LTLold of s1 implies ( the_left_argument_of H in the LTLold of s1 & H in the LTLold of s2 ) )
assume that
A1: ( s1 is_next_of s0 & s2 is_next_of s1 & H in the LTLold of s1 ) and
A2: H is Until ; :: thesis: ( the_right_argument_of H in the LTLold of s1 or ( the_left_argument_of H in the LTLold of s1 & H in the LTLold of s2 ) )
set G = the_right_argument_of H;
set F = the_left_argument_of H;
H = (the_left_argument_of H) 'U' (the_right_argument_of H) by A2, MODELC_2:8;
hence ( the_right_argument_of H in the LTLold of s1 or ( the_left_argument_of H in the LTLold of s1 & H in the LTLold of s2 ) ) by A1, Lm29; :: thesis: verum