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} )
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));
H in Subformulae H by MODELC_2:def 24;
then A1: {H} c= Subformulae H by ZFMISC_1:31;
assume A2: ( 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}
then the_right_argument_of H is_immediate_constituent_of H by 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 ;
then A3: Subformulae (the_right_argument_of H) c= Subformulae H by MODELC_2:46;
the_left_argument_of H is_immediate_constituent_of H by A2, 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 ;
then Subformulae (the_left_argument_of H) c= Subformulae H by MODELC_2:46;
then (Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H)) c= Subformulae H by A3, XBOOLE_1:8;
then A4: ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H} c= Subformulae H by A1, XBOOLE_1:8;
for x being object 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 object ; :: 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
A5: F = x and
A6: F is_subformula_of H by MODELC_2:def 24;

now :: thesis: x in ((Subformulae (the_left_argument_of H)) \/ (Subformulae (the_right_argument_of H))) \/ {H}

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 A5, 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 A6;
then ( F is_subformula_of the_left_argument_of H or F is_subformula_of the_right_argument_of H ) by A2, 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 A5, 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 A4; :: thesis: verum

end;

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