let H, F 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:73;
len (W \ {F}) = len L,(W \ {F}) by Deflen02, A2
.= len L,W by Thlen01, A1 ;
hence len (W \ {F}) = len W by Deflen02, A2; :: thesis: verum