let GX be non empty TopSpace; :: thesis: for V being Subset of GX st V is connected holds
Component_of V <> {}
let V be Subset of GX; :: thesis: ( V is connected implies Component_of V <> {} )
assume A1: V is connected ; :: thesis: Component_of V <> {}
per cases ( V = {} or V <> {} ) ;
suppose V = {} ; :: thesis: Component_of V <> {}
then V = {} GX ;
hence Component_of V <> {} by Th3; :: thesis: verum
end;
suppose V <> {} ; :: thesis: Component_of V <> {}
hence Component_of V <> {} by A1, Th1, XBOOLE_1:3; :: thesis: verum
end;
end;