reconsider G9 = G as Subgraph of G by Lm3;
take G9 ; :: thesis: G9 is spanning
thus G9 is spanning ; :: thesis: verum