let R be Relation; :: thesis: ( R is connected iff [:(),():] \ (id ()) c= R \/ (R ~) )
hereby :: thesis: ( [:(),():] \ (id ()) c= R \/ (R ~) implies R is connected )
assume R is connected ; :: thesis: [:(),():] \ (id ()) c= R \/ (R ~)
then A1: R is_connected_in field R ;
now :: thesis: for x being object st x in [:(),():] \ (id ()) holds
x in R \/ (R ~)
let x be object ; :: thesis: ( x in [:(),():] \ (id ()) implies x in R \/ (R ~) )
now :: thesis: ( x in [:(),():] \ (id ()) implies x in R \/ (R ~) )
assume A2: x in [:(),():] \ (id ()) ; :: thesis: x in R \/ (R ~)
then x in [:(),():] 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 () by ;
then y <> z by ;
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 ; :: thesis: verum
end;
hence ( x in [:(),():] \ (id ()) implies x in R \/ (R ~) ) ; :: thesis: verum
end;
hence [:(),():] \ (id ()) c= R \/ (R ~) ; :: thesis: verum
end;
assume A6: [:(),():] \ (id ()) 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 [:(),():] \ (id ()) implies [a,b] in R \/ (R ~) ) by A6;
then ( [a,b] in [:(),():] & not [a,b] in id () 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 ;
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