assume not Edges_In v,X is empty ; :: thesis: contradiction
then consider x being set such that
A1: x in Edges_In v,X by XBOOLE_0:def 1;
thus contradiction by A1, Def1; :: thesis: verum