:: deftheorem defines SubGraph SGRAPH1:def 7 :
for X being set
for G, b₃ being SimpleGraph of X holds
( b₃ is SubGraph of G iff ( the carrier of b₃ c= the carrier of G & the SEdges of b₃ c= the SEdges of G ) );