let H be LTL-formula; :: thesis: ( ( H is negative or H is next ) implies Subformulae H = (Subformulae (the_argument_of H)) \/ {H} )
set H1 = the_argument_of H;
H in Subformulae H by MODELC_2:45;
then A1: {H} c= Subformulae H by ZFMISC_1:31;
assume A2: ( H is negative or H is next ) ; :: thesis: Subformulae H = (Subformulae (the_argument_of H)) \/ {H}
then the_argument_of H is_immediate_constituent_of H by 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 ;
then Subformulae (the_argument_of H) c= Subformulae H by MODELC_2:46;
then A3: (Subformulae (the_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_argument_of H)) \/ {H} )

proof

let x be object ; :: 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
A4: F = x and
A5: F is_subformula_of H by MODELC_2:def 24;

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

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 A4, 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 A5;
then F is_subformula_of the_argument_of H by A2, 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 A4, 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 A3; :: thesis: verum

end;

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