let R be Relation; :: thesis: ( R is connected implies R ~ is connected )
assume A1: for x, y being set st x in field R & y in field R & x <> y & not [x,y] in R holds
[y,x] in R ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: R ~ is connected
let x be set ; :: according to RELAT_2:def 6,RELAT_2:def 14 :: thesis: for b₁ being set holds
( not x in field (R ~) or not b₁ in field (R ~) or x = b₁ or [x,b₁] in R ~ or [b₁,x] in R ~ )
let y be set ; :: thesis: ( not x in field (R ~) or not y in field (R ~) or x = y or [x,y] in R ~ or [y,x] in R ~ )
assume that
A2: x in field (R ~) and
A3: y in field (R ~) and
A4: x <> y ; :: thesis: ( [x,y] in R ~ or [y,x] in R ~ )
field R = field (R ~) by RELAT_1:21;
then ( [x,y] in R or [y,x] in R ) by A1, A2, A3, A4;
hence ( [x,y] in R ~ or [y,x] in R ~ ) by RELAT_1:def 7; :: thesis: verum