let T1, T2 be TopSpace; :: thesis: ( [:T1,T2:] is with_finite_small_inductive_dimension implies ( [:T2,T1:] is with_finite_small_inductive_dimension & ind [:T1,T2:] = ind [:T2,T1:] ) )
assume A1: [:T1,T2:] is with_finite_small_inductive_dimension ; :: thesis: ( [:T2,T1:] is with_finite_small_inductive_dimension & ind [:T1,T2:] = ind [:T2,T1:] )

per cases ( T1 is empty or T2 is empty or ( not T1 is empty & not T2 is empty ) ) ;

suppose A2: ( T1 is empty or T2 is empty ) ; :: thesis: ( [:T2,T1:] is with_finite_small_inductive_dimension & ind [:T1,T2:] = ind [:T2,T1:] )

then ind [:T1,T2:] = - 1 by Th6;
hence ( [:T2,T1:] is with_finite_small_inductive_dimension & ind [:T1,T2:] = ind [:T2,T1:] ) by A2, Th6; :: thesis: verum

end;

suppose ( not T1 is empty & not T2 is empty ) ; :: thesis: ( [:T2,T1:] is with_finite_small_inductive_dimension & ind [:T1,T2:] = ind [:T2,T1:] )

then [:T1,T2:],[:T2,T1:] are_homeomorphic by YELLOW12:44;
hence ( [:T2,T1:] is with_finite_small_inductive_dimension & ind [:T1,T2:] = ind [:T2,T1:] ) by A1, Lm9; :: thesis: verum

end;

end;