let n be Element of NAT ; ( 2 <= n implies for A, B, P being Subset of (TOP-REAL n) st P is Bounded & A is_outside_component_of P & B is_outside_component_of P holds
A = B )
assume A1:
2 <= n
; for A, B, P being Subset of (TOP-REAL n) st P is Bounded & A is_outside_component_of P & B is_outside_component_of P holds
A = B
let A, B, P be Subset of (TOP-REAL n); ( P is Bounded & A is_outside_component_of P & B is_outside_component_of P implies A = B )
assume that
A2:
P is Bounded
and
A3:
A is_outside_component_of P
and
A4:
B is_outside_component_of P
; A = B
A5:
B is_a_component_of P `
by A4, Def4;
UBD P is_outside_component_of P
by A1, A2, Th76;
then A6:
UBD P is_a_component_of P `
by Def4;
A7:
not P ` is empty
by A1, A2, Th74, XXREAL_0:2;
then A8:
B <> {}
by A5, SPRECT_1:4;
A9:
B c= UBD P
by A4, Th27;
A10:
A c= UBD P
by A3, Th27;
A11:
A is_a_component_of P `
by A3, Def4;
then
A <> {}
by A7, SPRECT_1:4;
then
A = UBD P
by A11, A6, A10, GOBOARD9:1, XBOOLE_1:69;
hence
A = B
by A5, A8, A6, A9, GOBOARD9:1, XBOOLE_1:69; verum