:: deftheorem Def1 defines connected DILWORTH:def 1 :
for R being RelStr
for S being Subset of R holds
( S is connected iff the InternalRel of R is_connected_in S );