let R be Relation; :: thesis: ( 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 implies R is_connected_in field R ) & ( R is_connected_in field R implies R is connected ) & ( R is_connected_in field R implies 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 ) & ( ( 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 ) implies R is_connected_in field R ) ) by RELAT_2:def 6, 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 ) ; :: thesis: verum