let GX be non empty TopSpace; :: thesis: for A being Subset of GX
for B being non empty Subset of GX st A is_a_component_of B holds
A <> {}
let A be Subset of GX; :: thesis: for B being non empty Subset of GX st A is_a_component_of B holds
A <> {}
let B be non empty Subset of GX; :: thesis: ( A is_a_component_of B implies A <> {} )
assume A is_a_component_of B ; :: thesis: A <> {}
then consider B1 being Subset of (GX | B) such that
A1: B1 = A and
A2: B1 is a_component by CONNSP_1:def 6;
B1 <> {} (GX | B) by A2, CONNSP_1:32;
hence A <> {} by A1; :: thesis: verum