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