let R be Relation; :: thesis: for X being set st R is_connected_in X holds
R ~ is_connected_in X
let X be set ; :: thesis: ( R is_connected_in X implies R ~ is_connected_in X )
assume A1: for x, y being set st x in X & y in X & x <> y & not [x,y] in R holds
[y,x] in R ; :: according to RELAT_2:def 6 :: thesis: R ~ is_connected_in X
let x be set ; :: according to RELAT_2:def 6 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or x = b₁ or [x,b₁] in R ~ or [b₁,x] in R ~ )
let y be set ; :: thesis: ( not x in X or not y in X or x = y or [x,y] in R ~ or [y,x] in R ~ )
assume that
A2: x in X and
A3: y in X and
A4: x <> y ; :: thesis: ( [x,y] in R ~ or [y,x] in R ~ )
( [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