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 :: thesis: not W <> {} H
assume W <> {} H ; :: thesis: contradiction
then consider x being object such that
A2: x in W by XBOOLE_0:def 1;
x in Subformulae H by A2;
then reconsider x = x as LTL-formula by MODELC_2:1;
set X = {x};
A3: {x} c= W by A2, ZFMISC_1:31;
x is_subformula_of H by A2, MODELC_2:45;
then reconsider X = {x} as Subset of (Subformulae H) by Lm9;
len X = len x by Th14;
then A4: len X >= 1 by MODELC_2:3;
len X <= len W by A3, Th15;
hence contradiction by A1, A4, XXREAL_0:2; :: thesis: verum
end;
hence W = {} H ; :: thesis: verum