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