let L be FinSequence; :: thesis: for F, H being LTL-formula
for W being Subset of (Subformulae H) st not F in W holds
len (L,(W \ {F})) = len (L,W)
let F, H be LTL-formula; :: thesis: for W being Subset of (Subformulae H) st not F in W holds
len (L,(W \ {F})) = len (L,W)
let W be Subset of (Subformulae H); :: thesis: ( not F in W implies len (L,(W \ {F})) = len (L,W) )
assume A1: not F in W ; :: thesis: len (L,(W \ {F})) = len (L,W)
A2: for x being object st x in W holds
x in W \ {F}

proof

let x be object ; :: thesis: ( x in W implies x in W \ {F} )
assume A3: x in W ; :: thesis: x in W \ {F}
then not x in {F} by A1, TARSKI:def 1;
hence x in W \ {F} by A3, XBOOLE_0:def 5; :: thesis: verum

end;

for x being object st x in W \ {F} holds
x in W by XBOOLE_0:def 5;
hence len (L,(W \ {F})) = len (L,W) by A2, TARSKI:2; :: thesis: verum