:: deftheorem Def24 defines c= GRAPH_1:def 24 :
for G1, G2 being Graph holds
( G1 c= G2 iff G1 is Subgraph of G2 );