let F, G, H be LTL-formula; :: thesis: ( H is_immediate_constituent_of F 'R' G iff ( H = F or H = G ) )
thus ( not H is_immediate_constituent_of F 'R' G or H = F or H = G ) :: thesis: ( ( H = F or H = G ) implies H is_immediate_constituent_of F 'R' G )

proof

set Z = F 'R' G;

A1: now :: thesis: ( not F 'R' G = 'not' H & not F 'R' G = 'X' H )

assume A2: ( F 'R' G = 'not' H or F 'R' G = 'X' H ) ; :: thesis: contradiction
(F 'R' G) . 1 = 5 by Th12;
hence contradiction by A2, Th12; :: thesis: verum

end;

A3: now :: thesis: for H1 being LTL-formula holds
( not F 'R' G = H '&' H1 & not F 'R' G = H1 '&' H & not F 'R' G = H 'or' H1 & not F 'R' G = H1 'or' H & not F 'R' G = H 'U' H1 & not F 'R' G = H1 'U' H )

given H1 being LTL-formula such that A4: ( F 'R' G = H '&' H1 or F 'R' G = H1 '&' H or F 'R' G = H 'or' H1 or F 'R' G = H1 'or' H or F 'R' G = H 'U' H1 or F 'R' G = H1 'U' H ) ; :: thesis: contradiction
(F 'R' G) . 1 = 5 by Th12;
hence contradiction by A4, Th12; :: thesis: verum

end;

assume H is_immediate_constituent_of F 'R' G ; :: thesis: ( H = F or H = G )
then ( F 'R' G = 'not' H or F 'R' G = 'X' H or ex H1 being LTL-formula st
( F 'R' G = H '&' H1 or F 'R' G = H1 '&' H or F 'R' G = H 'or' H1 or F 'R' G = H1 'or' H or F 'R' G = H 'U' H1 or F 'R' G = H1 'U' H or F 'R' G = H 'R' H1 or F 'R' G = H1 'R' H ) ) ;
hence ( H = F or H = G ) by A1, A3, Lm15; :: thesis: verum

end;

thus ( ( H = F or H = G ) implies H is_immediate_constituent_of F 'R' G ) ; :: thesis: verum