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