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 S1[ Nat] means for W1 being Subset of (Subformulae H) st card W1 <= $1 & W c= W1 holds
len W <= len W1;
set k = card W1;
A1: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A2: S1[k] ; :: thesis: S1[k + 1]
S1[k + 1]
proof
let W1 be Subset of (Subformulae H); :: thesis: ( card W1 <= k + 1 & W c= W1 implies len W <= len W1 )
assume A3: card W1 <= k + 1 ; :: thesis: ( not W c= W1 or len W <= len W1 )
( W c= W1 implies len W <= len W1 )
proof
assume A4: W c= W1 ; :: thesis: len W <= len W1
now :: thesis: len W <= len W1
per cases ( W = W1 or W <> W1 ) ;
suppose W = W1 ; :: thesis: len W <= len W1
hence len W <= len W1 ; :: thesis: verum
end;
suppose W <> W1 ; :: thesis: len W <= len W1
then W c< W1 by A4, XBOOLE_0:def 8;
then consider x being object such that
A5: x in W1 and
A6: W c= W1 \ {x} by XBOOLE_0:8;
x in Subformulae H by A5;
then reconsider x = x as LTL-formula by MODELC_2:1;
set X = {x};
{x} c= W1 by A5, ZFMISC_1:31;
then card (W1 \ {x}) = (card W1) - (card {x}) by CARD_2:44
.= (card W1) - 1 by CARD_1:30 ;
then (card (W1 \ {x})) + 1 <= k + 1 by A3;
then card (W1 \ {x}) <= k by XREAL_1:6;
then len W <= len (W1 \ {x}) by A2, A6;
then A7: len W <= (len W1) - (len x) by A5, Th10;
(len W1) - (len x) <= len W1 by XREAL_1:43;
hence len W <= len W1 by A7, 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 S1[k + 1] ; :: thesis: verum
end;
A8: S1[ 0 ]
proof
let W1 be Subset of (Subformulae H); :: thesis: ( card W1 <= 0 & W c= W1 implies len W <= len W1 )
assume card W1 <= 0 ; :: thesis: ( not W c= W1 or len W <= len W1 )
then W1 = {} H ;
hence ( not W c= W1 or len W <= len W1 ) ; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A8, A1);
 then S1[ card W1] ;
hence ( W c= W1 implies len W <= len W1 ) ; :: thesis: verum