let H be LTL-formula; :: thesis: ( H is atomic implies Subformulae H = {H} )
assume H is atomic ; :: thesis: Subformulae H = {H}
then ex n being Nat st H = atom. n ;
then A1: len H = 1 by FINSEQ_1:40;
A2: for x being object st x in Subformulae H holds
x in {H}

proof

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

now :: thesis: not G <> H

assume G <> H ; :: thesis: contradiction
then G is_proper_subformula_of H by A4;
then len G < 1 by A1, MODELC_2:32;
hence contradiction by MODELC_2:3; :: thesis: verum

end;

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

end;

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

proof

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

end;

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