let T be TopSpace; :: thesis: for A, B being Subset of T st B is_a_component_of A holds
B is connected
let A, B be Subset of T; :: thesis: ( B is_a_component_of A implies B is connected )
assume B is_a_component_of A ; :: thesis: B is connected
then consider C being Subset of (T | A) such that
A1: C = B and
A2: C is a_component by CONNSP_1:def 6;
C is connected by A2, CONNSP_1:def 5;
hence B is connected by A1, CONNSP_1:23; :: thesis: verum