reconsider E = the carrier' of G as finite set by GRAPH_1:def 11;
reconsider V = the carrier of G as finite set by GRAPH_1:def 11;
the carrier of (AddNewEdge (v1,v2)) = V by Def7;
hence the carrier of (AddNewEdge (v1,v2)) is finite ; :: according to GRAPH_1:def 11 :: thesis: the carrier' of (AddNewEdge (v1,v2)) is finite
the carrier' of (AddNewEdge (v1,v2)) = E \/ { the carrier' of G} by Def7;
hence the carrier' of (AddNewEdge (v1,v2)) is finite ; :: thesis: verum