let GX be non empty TopSpace; :: thesis: ( ( for x, y being Point of GX holds x,y are_joined ) implies GX is connected )
assume for x, y being Point of GX holds x,y are_joined ; :: thesis: GX is connected
then ex x being Point of GX st
for y being Point of GX holds x,y are_joined by Th29;
hence GX is connected by Th28; :: thesis: verum