let F, H be LTL-formula; :: thesis: for W being Subset of (Subformulae H) st W = {F} holds
len W = len F
let W be Subset of (Subformulae H); :: thesis: ( W = {F} implies len W = len F )
assume A1: W = {F} ; :: thesis: len W = len F
then A2: F in W by TARSKI:def 1;

now :: thesis: for x being object holds not x in W \ {F}

assume ex x being object st x in W \ {F} ; :: thesis: contradiction
then consider x being set such that
A3: x in W \ {F} ;
x in W by A3, XBOOLE_0:def 5;
hence contradiction by A1, A3, XBOOLE_0:def 5; :: thesis: verum

end;

then A4: W \ {F} = {} H by XBOOLE_0:def 1;
len W = ((len W) - (len F)) + (len F)
.= (len (W \ {F})) + (len F) by A2, Th10
.= 0 + (len F) by A4, Th13 ;
hence len W = len F ; :: thesis: verum