let H be LTL-formula; :: thesis: for W being Subset of (Subformulae H) st len W < 1 holds
W = {} H
let W be Subset of (Subformulae H); :: thesis: ( len W < 1 implies W = {} H )
assume A1: len W < 1 ; :: thesis: W = {} H

now

assume W <> {} H ; :: thesis: contradiction
then consider x being set such that
B1: x in W by XBOOLE_0:def 1;
x in Subformulae H by B1;
then reconsider x = x as LTL-formula by MODELC_2:1;
set X = {x};
B2: {x} c= W by B1, ZFMISC_1:37;
x is_subformula_of H by B1, MODELC_2:45;
then reconsider X = {x} as Subset of (Subformulae H) by Lem104;
len X = len x by Thlen11;
then B3: len X >= 1 by MODELC_2:3;
len X <= len W by B2, Thlen12;
hence contradiction by B3, A1, XXREAL_0:2; :: thesis: verum

end;

hence W = {} H ; :: thesis: verum