let F, H be LTL-formula; :: thesis: for W, W1 being Subset of (Subformulae H) st W1 = W \/ {F} holds
len W1 <= (len W) + (len F)
let W, W1 be Subset of (Subformulae H); :: thesis: ( W1 = W \/ {F} implies len W1 <= (len W) + (len F) )
assume A1: W1 = W \/ {F} ; :: thesis: len W1 <= (len W) + (len F)

now :: thesis: len W1 <= (len W) + (len F)

per cases ( F in W or not F in W ) ;

suppose F in W ; :: thesis: len W1 <= (len W) + (len F)

then {F} c= W by ZFMISC_1:31;
then W1 = W by A1, XBOOLE_1:12;
hence len W1 <= (len W) + (len F) by XREAL_1:31; :: thesis: verum

end;

suppose not F in W ; :: thesis: len W1 <= (len W) + (len F)

hence len W1 <= (len W) + (len F) by A1, Th11; :: thesis: verum

end;

end;

end;

hence len W1 <= (len W) + (len F) ; :: thesis: verum