let n be Element of NAT ; :: thesis: for A, B being Subset of (TOP-REAL n) st B is_outside_component_of A holds
B c= A `
let A, B be Subset of (TOP-REAL n); :: thesis: ( B is_outside_component_of A implies B c= A ` )
assume B is_outside_component_of A ; :: thesis: B c= A `
then B is_a_component_of A ` by Def4;
hence B c= A ` by SPRECT_1:7; :: thesis: verum