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

proof

assume A0: H is_immediate_constituent_of F 'U' G ; :: thesis: ( H = F or H = G )
set Z = F 'U' G;
A1: ( F 'U' G = 'not' H or F 'U' G = 'X' H or ex H1 being LTL-formula st
( F 'U' G = H '&' H1 or F 'U' G = H1 '&' H or F 'U' G = H 'or' H1 or F 'U' G = H1 'or' H or F 'U' G = H 'U' H1 or F 'U' G = H1 'U' H or F 'U' G = H 'R' H1 or F 'U' G = H1 'R' H ) ) by A0, Def100;

A2: now

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

end;

now

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

end;

hence ( H = F or H = G ) by Lm13, A1, A2; :: thesis: verum

end;

thus ( ( H = F or H = G ) implies H is_immediate_constituent_of F 'U' G ) by Def100; :: thesis: verum