let R be Relation; :: thesis: for X being set st R is_connected_in X holds
R |_2 X is connected
let X be set ; :: thesis: ( R is_connected_in X implies R |_2 X is connected )
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 |_2 X 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 |_2 X) or not b₁ in field (R |_2 X) or x = b₁ or [x,b₁] in R |_2 X or [b₁,x] in R |_2 X )
let y be set ; :: thesis: ( not x in field (R |_2 X) or not y in field (R |_2 X) or x = y or [x,y] in R |_2 X or [y,x] in R |_2 X )
assume ( x in field (R |_2 X) & y in field (R |_2 X) & x <> y ) ; :: thesis: ( [x,y] in R |_2 X or [y,x] in R |_2 X )
then ( x in X & y in X & x <> y ) by WELLORD1:19;
then ( ( [x,y] in R or [y,x] in R ) & [x,y] in [:X,X:] & [y,x] in [:X,X:] ) by A1, ZFMISC_1:106;
hence ( [x,y] in R |_2 X or [y,x] in R |_2 X ) by XBOOLE_0:def 4; :: thesis: verum