let H, F 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;
A3: W \ {F} = {} H

proof

now

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

end;

hence W \ {F} = {} H by XBOOLE_0:def 1; :: thesis: verum

end;

len W = ((len W) - (len F)) + (len F)
.= (len (W \ {F})) + (len F) by A2, Thlen07
.= 0 + (len F) by Thlen10, A3 ;
hence len W = len F ; :: thesis: verum