:: deftheorem defines c= GLIB_000:def 35 :
for G1, G2 being _Graph holds
( G1 c= G2 iff G1 is Subgraph of G2 );