for GX being non empty TopSpace st ( for x, y being Point of GX holds x,y are_joined ) holds
GX is connected