let T be TopSpace; ( T is T_1 & ( for A, B being closed Subset of st A misses B holds
ex A', B' being closed Subset of st
( A' misses B' & A' \/ B' = [#] T & A c= A' & B c= B' ) ) implies ( T is with_finite_small_inductive_dimension & ind T <= 0 ) )
assume A1:
( T is T_1 & ( for A, B being closed Subset of st A misses B holds
ex A', B' being closed Subset of st
( A' misses B' & A' \/ B' = [#] T & A c= A' & B c= B' ) ) )
; ( T is with_finite_small_inductive_dimension & ind T <= 0 )
A2:
now let p be
Point of ;
for U being open Subset of st p in U holds
ex W being open Subset of st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )let U be
open Subset of ;
( p in U implies ex W being open Subset of st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 ) )assume A3:
p in U
;
ex W being open Subset of st
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )reconsider P =
{p} as
Subset of
by A3, ZFMISC_1:37;
not
p in U `
by A3, XBOOLE_0:def 5;
then A4:
P misses U `
by ZFMISC_1:56;
not
T is
empty
by A3;
then consider A',
B' being
closed Subset of
such that A5:
A' misses B'
and A6:
A' \/ B' = [#] T
and A7:
P c= A'
and A8:
U ` c= B'
by A1, A4;
reconsider W =
B' ` as
open Subset of ;
take W =
W;
( p in W & W c= U & Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )
p in P
by TARSKI:def 1;
then
(
(U ` ) ` = U & not
p in B' )
by A5, A7, XBOOLE_0:3;
hence
(
p in W &
W c= U )
by A3, A8, SUBSET_1:31, XBOOLE_0:def 5;
( Fr W is with_finite_small_inductive_dimension & ind (Fr W) <= 0 - 1 )
B' = A' `
by A5, A6, PRE_TOPC:25;
then
Fr B' = {} T
by TOPGEN_1:16;
hence
(
Fr W is
with_finite_small_inductive_dimension &
ind (Fr W) <= 0 - 1 )
by Th6;
verum end;
then
T is with_finite_small_inductive_dimension
by Th15;
hence
( T is with_finite_small_inductive_dimension & ind T <= 0 )
by A2, Th16; verum