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