let F, H be LTL-formula; :: thesis: for W being Subset of (Subformulae H) st not F in W holds
len (W \ {F}) = len W
let W be Subset of (Subformulae H); :: thesis: ( not F in W implies len (W \ {F}) = len W )
assume A1: not F in W ; :: thesis: len (W \ {F}) = len W
consider L being FinSequence such that
A2: ( rng L = Subformulae H & L is one-to-one ) by FINSEQ_4:58;
len (W \ {F}) = len (L,(W \ {F})) by A2, Def26
.= len (L,W) by A1, Th5 ;
hence len (W \ {F}) = len W by A2, Def26; :: thesis: verum