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