let X be set ; :: thesis: for A being Subset of X
for O being Order of X st O is_connected_in X holds
O is_connected_in A
let A be Subset of X; :: thesis: for O being Order of X st O is_connected_in X holds
O is_connected_in A
let O be Order of X; :: thesis: ( O is_connected_in X implies O is_connected_in A )
assume O is_connected_in X ; :: thesis: O is_connected_in A
then for x, y being object st x in A & y in A & x <> y & not [x,y] in O holds
[y,x] in O by RELAT_2:def 6;
hence O is_connected_in A by RELAT_2:def 6; :: thesis: verum