reconsider G1 = G as Supergraph of G by Th62;
take G1 ; :: thesis: G1 is finite
thus G1 is finite ; :: thesis: verum