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 A3: x in [:(field R),(field R):] \ (id (field R)) ; :: thesis: x in R \/ (R ~)
then x in [:(field R),(field R):] by XBOOLE_0:def 5;
then consider y, z being set such that
A4: y in field R and
A5: z in field R and
A6: x = [y,z] by ZFMISC_1:def 2;
not x in id (field R) by A3, XBOOLE_0:def 5;
then y <> z by A4, A6, RELAT_1:def 10;
then ( [y,z] in R or [z,y] in R ) by A2, A4, A5, Def6;
then ( [y,z] in R or [y,z] in R ~ ) by RELAT_1:def 7;
hence x in R \/ (R ~) by A6, 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 A7: [:(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 )
( [a,b] in [:(field R),(field R):] \ (id (field R)) implies [a,b] in R \/ (R ~) ) by A7;
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 A8: ( 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:87;
assume ( a in field R & b in field R & a <> b ) ; :: thesis: ( [a,b] in R or [b,a] in R )
hence ( [a,b] in R or [b,a] in R ) by A8, 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