take G = MultiGraphStruct(# 1,1,op1,op1 #); :: thesis: G is finite
thus the carrier of G is finite ; :: according to GRAPH_1:def 9 :: thesis: the carrier' of G is finite
thus the carrier' of G is finite ; :: thesis: verum