let G be Graph; :: thesis: for v being Vertex of G
for X being set holds Edges_Out v,X c= Edges_Out v
let v be Vertex of G; :: thesis: for X being set holds Edges_Out v,X c= Edges_Out v
let X be set ; :: thesis: Edges_Out v,X c= Edges_Out v
let e be set ; :: according to TARSKI:def 3 :: thesis: ( not e in Edges_Out v,X or e in Edges_Out v )
assume e in Edges_Out v,X ; :: thesis: e in Edges_Out v
then ( e in the carrier' of G & e in X & the Source of G . e = v ) by Def2;
hence e in Edges_Out v by Def2; :: thesis: verum