theorem :: GRAPH_1:3

for G being Graph
for v being set st v in the carrier' of G holds
( the Source of G . v in the carrier of G & the Target of G . v in the carrier of G ) by FUNCT_2:5;