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 object ; :: according to TARSKI:def 3 :: thesis: ( not e in Edges_Out (v,X) or e in Edges_Out v )
assume A1: e in Edges_Out (v,X) ; :: thesis: e in Edges_Out v
then the Source of G . e = v by Def2;
hence e in Edges_Out v by A1, Def2; :: thesis: verum