let n be Element of NAT ; :: thesis: ( 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 ; :: thesis: 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); :: thesis: ( 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 & B is_outside_component_of P ) ; :: thesis: A = B
A4: UBD P is_outside_component_of P by A1, A2, Th76;
A5: ( A is_a_component_of P ` & B is_a_component_of P ` ) by A3, Def4;
not P ` is empty by A1, A2, Th74, XXREAL_0:2;
then A6: ( A <> {} & B <> {} ) by A5, SPRECT_1:6;
A7: UBD P is_a_component_of P ` by A4, Def4;
( A c= UBD P & B c= UBD P ) by A3, Th27;
then ( A = UBD P & B = UBD P ) by A5, A6, A7, GOBOARD9:3, XBOOLE_1:69;
hence A = B ; :: thesis: verum