let H be LTL-formula; :: thesis: ( H is atomic implies Subformulae H = {H} )
assume H is atomic ; :: thesis: Subformulae H = {H}
then consider n being Nat such that
A01: H = atom. n by MODELC_2:def 11;
A02: len H = 1 by A01, FINSEQ_1:57;
A1: for x being set st x in {H} holds
x in Subformulae H

proof

let x be set ; :: thesis: ( x in {H} implies x in Subformulae H )
assume x in {H} ; :: thesis: x in Subformulae H
then B1: x = H by TARSKI:def 1;
H is_subformula_of H by MODELC_2:27;
hence x in Subformulae H by B1, MODELC_2:45; :: thesis: verum

end;

for x being set st x in Subformulae H holds
x in {H}

proof

let x be set ; :: thesis: ( x in Subformulae H implies x in {H} )
assume x in Subformulae H ; :: thesis: x in {H}
then consider G being LTL-formula such that
B1: G = x and
B2: G is_subformula_of H by MODELC_2:def 24;
G = H

proof

now

assume G <> H ; :: thesis: contradiction
then G is_proper_subformula_of H by B2, MODELC_2:def 23;
then len G < 1 by A02, MODELC_2:32;
hence contradiction by MODELC_2:3; :: thesis: verum

end;

hence G = H ; :: thesis: verum

end;

hence x in {H} by B1, TARSKI:def 1; :: thesis: verum

end;

hence Subformulae H = {H} by A1, TARSKI:2; :: thesis: verum