let H, v be LTL-formula; :: thesis: for s1, s0, s2 being strict elementary LTLnode of 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 s1, s0, s2 be strict elementary LTLnode of 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, Lm30; :: thesis: verum