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 ) ;
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