let X be object ; :: thesis: 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 )
let R be Relation; :: thesis: ( 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 )
thus ( R is connected implies 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 ) by RELAT_2:def 6, RELAT_2:def 14; :: thesis: ( ( 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 ) implies R is connected )
assume A1: 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 ; :: thesis: R is connected
set X = field R;
for x, y being object st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R by A1;
hence R is connected by RELAT_2:def 14, RELAT_2:def 6; :: thesis: verum