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

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

hence
contradiction
by CHORD:def 6; :: thesis: verumv1,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;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