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
A2: field R = field (R ~ ) by RELAT_1:38;
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 ( x in field (R ~ ) & y in field (R ~ ) & x <> y ) ; :: thesis: ( [x,y] in R ~ or [y,x] in R ~ )
then ( [x,y] in R or [y,x] in R ) by A1, A2;
hence ( [x,y] in R ~ or [y,x] in R ~ ) by RELAT_1:def 7; :: thesis: verum