let R be Relation; ( R is connected iff for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R )
( R is connected iff R is_connected_in field R )
by RELAT_2:def 14;
hence
( R is connected iff for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R )
by RELAT_2:def 6; verum