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
assume A2: not A <> {} GX ; :: thesis: contradiction
consider x being Point of GX;
A3: {x} is connected by Th29;
{} c= {x} by XBOOLE_1:2;
hence contradiction by A1, A2, A3, Def5; :: thesis: verum