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

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

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

assume A6:
[:(field R),(field R):] \ (id (field R)) c= R \/ (R ~)
; :: thesis: 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 ;

end;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 ~)

hence
[:(field R),(field R):] \ (id (field R)) c= R \/ (R ~)
; :: thesis: verumx in R \/ (R ~)

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

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

hence
( x in [:(field R),(field R):] \ (id (field R)) implies x in R \/ (R ~) )
; :: thesis: verumassume 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;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

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