let L be FinSequence; :: thesis: for H, F being LTL-formula
for W being Subset of (Subformulae H) st not F in W holds
len L,(W \ {F}) = len L,W
let H, F 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 set st x in W \ {F} holds
x in W by XBOOLE_0:def 5;
for x being set st x in W holds
x in W \ {F}

proof

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

end;

hence len L,(W \ {F}) = len L,W by A2, TARSKI:2; :: thesis: verum