let H be LTL-formula; :: thesis: ( ( H is negative or H is next ) implies Subformulae H = (Subformulae (the_argument_of H)) \/ {H} )
assume A0: ( H is negative or H is next ) ; :: thesis: Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
set H1 = the_argument_of H;
the_argument_of H is_immediate_constituent_of H by A0, MODELC_2:20, MODELC_2:21;
then the_argument_of H is_proper_subformula_of H by MODELC_2:29;
then the_argument_of H is_subformula_of H by MODELC_2:def 23;
then A1: Subformulae (the_argument_of H) c= Subformulae H by MODELC_2:46;
H is_subformula_of H by MODELC_2:27;
then H in Subformulae H by MODELC_2:45;
then {H} c= Subformulae H by ZFMISC_1:37;
then A2: (Subformulae (the_argument_of H)) \/ {H} c= Subformulae H by A1, XBOOLE_1:8;
for x being set holds
( x in Subformulae H iff x in (Subformulae (the_argument_of H)) \/ {H} )

proof

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

proof

assume x in Subformulae H ; :: thesis: x in (Subformulae (the_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_argument_of H)) \/ {H}

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

end;

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

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

end;

end;

end;

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

end;

hence ( x in Subformulae H iff x in (Subformulae (the_argument_of H)) \/ {H} ) by A2; :: thesis: verum

end;

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