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

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