:: deftheorem Def11 defines finite GRAPH_1:def 11 :
for IT being MultiGraphStruct holds
( IT is finite iff ( the carrier of IT is finite & the carrier' of IT is finite ) );