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