assume not Edges_In v,X is empty ; :: thesis: contradiction
then ex x being set st x in Edges_In v,X by XBOOLE_0:def 1;
hence contradiction by Def1; :: thesis: verum