:: deftheorem defines c< GLIB_000:def 36 :
for G1, G2 being _Graph holds
( G1 c< G2 iff ( G1 c= G2 & G1 != G2 ) );