let X, Y be set ; :: thesis: for R being Relation st R is_connected_in X & Y c= X holds
R is_connected_in Y
let R be Relation; :: thesis: ( R is_connected_in X & Y c= X implies R is_connected_in Y )
assume A1: ( R is_connected_in X & Y c= X ) ; :: thesis: R is_connected_in Y
let x be set ; :: according to RELAT_2:def 6 :: thesis: for b₁ being set holds
( not x in Y or not b₁ in Y or x = b₁ or [x,b₁] in R or [b₁,x] in R )
let y be set ; :: thesis: ( not x in Y or not y in Y or x = y or [x,y] in R or [y,x] in R )
assume ( x in Y & y in Y ) ; :: thesis: ( x = y or [x,y] in R or [y,x] in R )
hence ( x = y or [x,y] in R or [y,x] in R ) by A1, RELAT_2:def 6; :: thesis: verum