:: deftheorem defines connected GRAPH_1:def 10 :
for IT being Graph holds
( IT is connected iff for G1, G2 being Graph holds
( not the carrier of G1 misses the carrier of G2 or not IT is_sum_of G1,G2 ) );