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;