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