:: deftheorem Def4 defines are_joined CONNSP_1:def 4 :
for GX being TopStruct
for x, y being Point of GX holds
( x,y are_joined iff ex C being Subset of GX st
( C is connected & x in C & y in C ) );