let n be 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;
UBD P is_outside_component_of P
by A1, A2, Th53;
then A6:
UBD P is_a_component_of P `
;
A7:
not P ` is empty
by A1, A2, Th51, XXREAL_0:2;
A8:
B <> {}
by A4;
A9:
B c= UBD P
by A4, Th14;
A10:
A c= UBD P
by A3, Th14;
A11:
A is_a_component_of P `
by A3;
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