let G2 be Subgraph of G; :: thesis: ( G2 is spanning implies not G2 is complete )
assume A1: G2 is spanning ; :: thesis: not G2 is complete
assume A2: G2 is complete ; :: thesis: contradiction

now :: thesis: for v1, w1 being Vertex of G st v1 <> w1 holds
v1,w1 are_adjacent

let v1, w1 be Vertex of G; :: thesis: ( v1 <> w1 implies v1,w1 are_adjacent )
assume A3: v1 <> w1 ; :: thesis: v1,w1 are_adjacent
reconsider v2 = v1, w2 = w1 as Vertex of G2 by A1, GLIB_000:def 33;
consider e being object such that
A4: e Joins v2,w2,G2 by A2, A3, CHORD:def 6, CHORD:def 3;
thus v1,w1 are_adjacent by A4, GLIB_000:72, CHORD:def 3; :: thesis: verum

end;

hence contradiction by CHORD:def 6; :: thesis: verum