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