let T be TopSpace; :: thesis: for A being finite Subset of T holds ind A < card A
let A be finite Subset of T; :: thesis: ind A < card A
A in (Seq_of_ind T) . (card A) by Lm1;
then A1: ind A <= (card A) - 1 by Th7;
(card A) - 1 < (card A) - 0 by XREAL_1:15;
hence ind A < card A by A1, XXREAL_0:2; :: thesis: verum