let H be LTL-formula; :: thesis: for W, W1 being Subset of (Subformulae H) st W c= W1 holds
len W <= len W1
let W, W1 be Subset of (Subformulae H); :: thesis: ( W c= W1 implies len W <= len W1 )
defpred S₁[ Nat] means for W1 being Subset of (Subformulae H) st card W1 <= $1 & W c= W1 holds
len W <= len W1;
A1: S₁[ 0 ]

proof

let W1 be Subset of (Subformulae H); :: thesis: ( card W1 <= 0 & W c= W1 implies len W <= len W1 )
assume B1: card W1 <= 0 ; :: thesis: ( not W c= W1 or len W <= len W1 )
W1 = {} H by B1;
hence ( not W c= W1 or len W <= len W1 ) ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: S₁[k] ; :: thesis: S₁[k + 1]
S₁[k + 1]

proof

let W1 be Subset of (Subformulae H); :: thesis: ( card W1 <= k + 1 & W c= W1 implies len W <= len W1 )
assume B2: card W1 <= k + 1 ; :: thesis: ( not W c= W1 or len W <= len W1 )
( W c= W1 implies len W <= len W1 )

proof

assume C1: W c= W1 ; :: thesis: len W <= len W1

now

per cases ( W = W1 or ex x being set st
( x in W1 & W c= W1 \ {x} ) ) by C1, lemlen05;

suppose W = W1 ; :: thesis: len W <= len W1

hence len W <= len W1 ; :: thesis: verum

end;

suppose ex x being set st
( x in W1 & W c= W1 \ {x} ) ; :: thesis: len W <= len W1

then consider x being set such that
D1: ( x in W1 & W c= W1 \ {x} ) ;
x in Subformulae H by D1;
then reconsider x = x as LTL-formula by MODELC_2:1;
set X = {x};
{x} c= W1 by D1, ZFMISC_1:37;
then card (W1 \ {x}) = (card W1) - (card {x}) by CARD_2:63
.= (card W1) - 1 by CARD_1:50 ;
then (card (W1 \ {x})) + 1 <= k + 1 by B2;
then card (W1 \ {x}) <= k by XREAL_1:8;
then len W <= len (W1 \ {x}) by B1, D1;
then D3: len W <= (len W1) - (len x) by D1, Thlen07;
(len W1) - (len x) <= len W1 by XREAL_1:45;
hence len W <= len W1 by D3, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence len W <= len W1 ; :: thesis: verum

end;

hence ( not W c= W1 or len W <= len W1 ) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A3: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A2);
set k = card W1;
S₁[ card W1] by A3;
hence ( W c= W1 implies len W <= len W1 ) ; :: thesis: verum