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