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 Deflen02, A1;
hence len ({} H) = 0 by Thlen00; :: thesis: verum