let R be Relation; :: thesis: ( R is connected iff [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~ ) )

A1: now

assume R is connected ; :: thesis: [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~ )
then A2: R is_connected_in field R by Def14;

now

let x be set ; :: thesis: ( x in [:(field R),(field R):] \ (id (field R)) implies x in R \/ (R ~ ) )

now

assume x in [:(field R),(field R):] \ (id (field R)) ; :: thesis: x in R \/ (R ~ )
then A3: ( x in [:(field R),(field R):] & not x in id (field R) ) by XBOOLE_0:def 5;
then consider y, z being set such that
A4: ( y in field R & z in field R & x = [y,z] ) by ZFMISC_1:def 2;
y <> z by A3, A4, RELAT_1:def 10;
then ( [y,z] in R or [z,y] in R ) by A2, A4, Def6;
then ( [y,z] in R or [y,z] in R ~ ) by RELAT_1:def 7;
hence x in R \/ (R ~ ) by A4, XBOOLE_0:def 3; :: thesis: verum

end;

hence ( x in [:(field R),(field R):] \ (id (field R)) implies x in R \/ (R ~ ) ) ; :: thesis: verum

end;

hence [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~ ) by TARSKI:def 3; :: thesis: verum

end;

now

assume A5: [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~ ) ; :: thesis: R is connected

now

let a, b be set ; :: thesis: ( a in field R & b in field R & a <> b & not [a,b] in R implies [b,a] in R )
assume A6: ( a in field R & b in field R & a <> b ) ; :: thesis: ( [a,b] in R or [b,a] in R )
( [a,b] in [:(field R),(field R):] \ (id (field R)) implies [a,b] in R \/ (R ~ ) ) by A5;
then ( [a,b] in [:(field R),(field R):] & not [a,b] in id (field R) implies [a,b] in R \/ (R ~ ) ) by XBOOLE_0:def 5;
then ( a in field R & b in field R & a <> b & not [a,b] in R implies [a,b] in R ~ ) by RELAT_1:def 10, XBOOLE_0:def 3, ZFMISC_1:106;
hence ( [a,b] in R or [b,a] in R ) by A6, RELAT_1:def 7; :: thesis: verum

end;

then R is_connected_in field R by Def6;
hence R is connected by Def14; :: thesis: verum

end;

hence ( R is connected iff [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~ ) ) by A1; :: thesis: verum