let GX be non empty TopSpace; :: thesis: for A being Subset of GX st A is_a_component_of GX holds
A <> {} GX
let A be Subset of GX; :: thesis: ( A is_a_component_of GX implies A <> {} GX )
assume A1: A is_a_component_of GX ; :: thesis: A <> {} GX
consider x being Point of GX;
A2: {} c= {x} by XBOOLE_1:2;
A3: {x} is connected by Th29;
assume not A <> {} GX ; :: thesis: contradiction
hence contradiction by A1, A3, A2, Def5; :: thesis: verum