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