set iG1 = (ind G1) + 1;
set iG2 = (ind G2) + 1;
- 1 <= ind G1 by Def6;
then (- 1) + 1 <= (ind G1) + 1 by XREAL_1:6;
then A1: (ind G1) + 1 in NAT by INT_1:3;
- 1 <= ind G2 by Def6;
then (- 1) + 1 <= (ind G2) + 1 by XREAL_1:6;
then A2: (ind G2) + 1 in NAT by INT_1:3;
then ( (ind G1) + 0 <= (ind G1) + 1 & (ind G1) + 1 <= ((ind G1) + 1) + ((ind G2) + 1) ) by A1, NAT_1:11, XREAL_1:6;
then A3: ind G1 <= ((ind G1) + 1) + ((ind G2) + 1) by XXREAL_0:2;
( (ind G2) + 0 <= (ind G2) + 1 & (ind G2) + 1 <= ((ind G2) + 1) + ((ind G1) + 1) ) by A2, A1, NAT_1:11, XREAL_1:6;
then ind G2 <= ((ind G1) + 1) + ((ind G2) + 1) by XXREAL_0:2;
hence for b₁ being Subset-Family of T st b₁ = G1 \/ G2 holds
b₁ is with_finite_small_inductive_dimension by A3, Lm4; :: thesis: verum