:: deftheorem Def18 defines Subgraph GRAPH_1:def 18 :
for G, b₂ being Graph holds
( b₂ is Subgraph of G iff ( the carrier of b₂ c= the carrier of G & the carrier' of b₂ c= the carrier' of G & ( for v being set st v in the carrier' of b₂ holds
( the Source of b₂ . v = the Source of G . v & the Target of b₂ . v = the Target of G . v & the Source of G . v in the carrier of b₂ & the Target of G . v in the carrier of b₂ ) ) ) );