let H be LTL-formula; :: thesis: len ({} H) = 0
consider L being FinSequence such that
A1: ( rng L = Subformulae H & L is one-to-one ) by FINSEQ_4:73;
len ({} H) = len L,({} H) by A1, Def26;
hence len ({} H) = 0 by Th4; :: thesis: verum