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