let T be TopSpace; :: thesis: for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat

let Af be finite-ind Subset of T; :: thesis: (ind Af) + 1 is Nat

Af in (Seq_of_ind T) . (1 + (ind Af)) by TOPDIM_1:def 5;

then (ind Af) + 1 in dom (Seq_of_ind T) by FUNCT_1:def 2;

hence (ind Af) + 1 is Nat ; :: thesis: verum

let Af be finite-ind Subset of T; :: thesis: (ind Af) + 1 is Nat

Af in (Seq_of_ind T) . (1 + (ind Af)) by TOPDIM_1:def 5;

then (ind Af) + 1 in dom (Seq_of_ind T) by FUNCT_1:def 2;

hence (ind Af) + 1 is Nat ; :: thesis: verum