theorem LemCon: :: PREFER_1:33

for X being object
for R being Relation holds
( R is connected iff for x, y being object st x <> y & x in field R & y in field R & not [x,y] in R holds
[y,x] in R )