let H be LTL-formula; :: thesis: ( ( H is conjunctive or H is disjunctive or H is Until or H is Release ) implies Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} )
assume A0: ( H is conjunctive or H is disjunctive or H is Until or H is Release ) ; :: thesis: Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
set H1 = the_left_argument_of H;
set H2 = the_right_argument_of H;
set SUBF = (Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H));
the_left_argument_of H is_immediate_constituent_of H by A0, MODELC_2:22, MODELC_2:23, MODELC_2:24, MODELC_2:25;
then the_left_argument_of H is_proper_subformula_of H by MODELC_2:29;
then the_left_argument_of H is_subformula_of H by MODELC_2:def 23;
then A1: Subformulae (the_left_argument_of H) c= Subformulae H by MODELC_2:46;
the_right_argument_of H is_immediate_constituent_of H by A0, MODELC_2:22, MODELC_2:23, MODELC_2:24, MODELC_2:25;
then the_right_argument_of H is_proper_subformula_of H by MODELC_2:29;
then the_right_argument_of H is_subformula_of H by MODELC_2:def 23;
then Subformulae (the_right_argument_of H) c= Subformulae H by MODELC_2:46;
then A2: (Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H)) c= Subformulae H by A1, XBOOLE_1:8;
H is_subformula_of H by MODELC_2:27;
then H in Subformulae H by MODELC_2:def 24;
then {H} c= Subformulae H by ZFMISC_1:37;
then A3: ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} c= Subformulae H by A2, XBOOLE_1:8;
for x being set holds
( x in Subformulae H iff x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} )

proof

let x be set ; :: thesis: ( x in Subformulae H iff x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} )
( x in Subformulae H implies x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} )

proof

assume x in Subformulae H ; :: thesis: x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}
then consider F being LTL-formula such that
B1: F = x and
B2: F is_subformula_of H by MODELC_2:def 24;

now

per cases ( F = H or F <> H ) ;

suppose F = H ; :: thesis: x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}

then F in {H} by TARSKI:def 1;
hence x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by B1, XBOOLE_0:def 3; :: thesis: verum

end;

suppose F <> H ; :: thesis: x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}

then F is_proper_subformula_of H by B2, MODELC_2:def 23;
then ( F is_subformula_of the_left_argument_of H or F is_subformula_of the_right_argument_of H ) by A0, MODELC_2:38;
then ( F in Subformulae (the_left_argument_of H) or F in Subformulae (the_right_argument_of H) ) by MODELC_2:45;
then F in (Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H)) by XBOOLE_0:def 3;
hence x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by B1, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} ; :: thesis: verum

end;

hence ( x in Subformulae H iff x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} ) by A3; :: thesis: verum

end;

hence Subformulae H = ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} by TARSKI:2; :: thesis: verum