let H, F 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

assume H is_immediate_constituent_of 'X' F ; :: thesis: H = F
then A1: ( '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 ) ) by Def100;

A2: now

assume A3: 'X' F = 'not' H ; :: thesis: contradiction
( ('X' F) . 1 = 3 & ('not' H) . 1 = 0 ) by Th100;
hence contradiction by A3; :: thesis: verum

end;

A4: now

given H1 being LTL-formula such that A5: ( '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 & (H '&' H1) . 1 = 1 & (H1 '&' H) . 1 = 1 & (H 'or' H1) . 1 = 2 & (H1 'or' H) . 1 = 2 & (H 'U' H1) . 1 = 4 & (H1 'U' H) . 1 = 4 & (H 'R' H1) . 1 = 5 & (H1 'R' H) . 1 = 5 ) by Th100;
hence contradiction by A5; :: thesis: verum

end;

thus H = F by A1, A2, A4, FINSEQ_1:46; :: thesis: verum

end;

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