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

hereby :: thesis: ( [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) implies R is connected )

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

now :: thesis: for x being object st x in [:(field R),(field R):] \ (id (field R)) holds
x in R \/ (R ~)

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

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

assume A2: 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 object such that
A3: y in field R and
A4: z in field R and
A5: x = [y,z] by ZFMISC_1:def 2;
not x in id (field R) by A2, XBOOLE_0:def 5;
then y <> z by A3, A5, RELAT_1:def 10;
then ( [y,z] in R or [z,y] in R ) by A1, A3, A4;
then ( [y,z] in R or [y,z] in R ~ ) by RELAT_1:def 7;
hence x in R \/ (R ~) by A5, 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 ~) ; :: thesis: verum

end;

assume A6: [:(field R),(field R):] \ (id (field R)) c= R \/ (R ~) ; :: thesis: R is connected
let a be object ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: for y being object st a in field R & y in field R & a <> y & not [a,y] in R holds
[y,a] in R
let b be object ; :: 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 A6;
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:87;
hence ( a in field R & b in field R & a <> b & not [a,b] in R implies [b,a] in R ) by RELAT_1:def 7; :: thesis: verum