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