let n, m be Nat; :: thesis: for T being non empty TopSpace
for A, B being Subset of T
for r, s being Real st r > 0 & s > 0 holds
for pA being Point of ()
for pB being Point of () st T | A,() | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m

let T be non empty TopSpace; :: thesis: for A, B being Subset of T
for r, s being Real st r > 0 & s > 0 holds
for pA being Point of ()
for pB being Point of () st T | A,() | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m

let A, B be Subset of T; :: thesis: for r, s being Real st r > 0 & s > 0 holds
for pA being Point of ()
for pB being Point of () st T | A,() | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m

let r, s be Real; :: thesis: ( r > 0 & s > 0 implies for pA being Point of ()
for pB being Point of () st T | A,() | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m )

assume that
A1: r > 0 and
A2: s > 0 ; :: thesis: for pA being Point of ()
for pB being Point of () st T | A,() | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m

let pA be Point of (); :: thesis: for pB being Point of () st T | A,() | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B holds
n = m

let pB be Point of (); :: thesis: ( T | A,() | (Ball (pA,r)) are_homeomorphic & T | B, Tdisk (pB,s) are_homeomorphic & Int A meets Int B implies n = m )
assume that
A3: T | A,() | (Ball (pA,r)) are_homeomorphic and
A4: T | B, Tdisk (pB,s) are_homeomorphic and
A5: Int A meets Int B ; :: thesis: n = m
A6: Int A c= A by TOPS_1:16;
set TBALL = () | (Ball (pA,r));
consider hA being Function of (T | A),(() | (Ball (pA,r))) such that
A7: hA is being_homeomorphism by ;
A8: (Int A) /\ (Int B) c= Int A by XBOOLE_1:17;
A9: [#] (T | A) = A by PRE_TOPC:def 5;
then reconsider IA = (Int A) /\ (Int B) as Subset of (T | A) by ;
A10: (T | A) | IA = T | ((Int A) /\ (Int B)) by ;
A11: [#] (() | (Ball (pA,r))) = Ball (pA,r) by PRE_TOPC:def 5;
then reconsider hAI = hA .: IA as Subset of () by XBOOLE_1:1;
A12: (Int A) /\ (Int B) in the topology of T by PRE_TOPC:def 2;
not (Int A) /\ (Int B) is empty by A5;
then consider p being set such that
A13: p in (Int A) /\ (Int B) ;
reconsider p = p as Point of T by A13;
A14: dom hA = [#] (T | A) by ;
then A15: hA . p in hA .: IA by ;
p in Int A by ;
then not (TOP-REAL n) | (Ball (pA,r)) is empty by ;
then reconsider g = hA | IA as Function of ((T | A) | IA),((() | (Ball (pA,r))) | (hA .: IA)) by ;
A16: Int B c= B by TOPS_1:16;
IA /\ A = IA by ;
then IA in the topology of (T | A) by ;
then IA is open by PRE_TOPC:def 2;
then hA .: IA is open by ;
then hAI is open by ;
then not Int hAI is empty by ;
then A17: not hAI is boundary ;
consider hB being Function of (T | B),(Tdisk (pB,s)) such that
A18: hB is being_homeomorphism by ;
A19: ((TOP-REAL n) | (Ball (pA,r))) | (hA .: IA) = () | hAI by ;
then reconsider G = g as Function of (T | ((Int A) /\ (Int B))),(() | hAI) by A10;
A20: (Int A) /\ (Int B) c= Int B by XBOOLE_1:17;
A21: [#] (T | B) = B by PRE_TOPC:def 5;
then reconsider IB = (Int A) /\ (Int B) as Subset of (T | B) by ;
A22: (T | B) | IB = T | ((Int A) /\ (Int B)) by ;
A23: dom hB = [#] (T | B) by ;
then A24: hB . p in hB .: IB by ;
p in Int B by ;
then not Tdisk (pB,s) is empty by ;
then reconsider f = hB | IB as Function of ((T | B) | IB),((Tdisk (pB,s)) | (hB .: IB)) by ;
A25: [#] (Tdisk (pB,s)) = cl_Ball (pB,s) by PRE_TOPC:def 5;
then reconsider hBI = hB .: IB as Subset of () by XBOOLE_1:1;
A26: (Tdisk (pB,s)) | (hB .: IB) = () | hBI by ;
then reconsider F = f as Function of (T | ((Int A) /\ (Int B))),(() | hBI) by A22;
F is being_homeomorphism by ;
then A27: F " is being_homeomorphism by ;
reconsider GF = G * (F ") as Function of (() | hBI),(() | hAI) by A13;
G is being_homeomorphism by ;
then GF is being_homeomorphism by ;
then hBI,hAI are_homeomorphic by ;
then A28: ind hBI = ind hAI by TOPDIM_1:27;
IB /\ B = IB by ;
then IB in the topology of (T | B) by ;
then IB is open by PRE_TOPC:def 2;
then hB .: IB is open by ;
then not Int hBI is empty by ;
then not hBI is boundary ;
then ind hBI = m by Th6;
hence n = m by ; :: thesis: verum