let F, H be LTL-formula; :: thesis: ( H is_immediate_constituent_of 'X' F iff H = F )
thus ( H is_immediate_constituent_of 'X' F implies H = F ) :: thesis: ( H = F implies H is_immediate_constituent_of 'X' F )

proof

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

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

end;

A3: now :: thesis: not 'X' F = 'not' H

assume A4: 'X' F = 'not' H ; :: thesis: contradiction
('X' F) . 1 = 3 by Th12;
hence contradiction by A4, Th12; :: thesis: verum

end;

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

end;

thus ( H = F implies H is_immediate_constituent_of 'X' F ) ; :: thesis: verum