let H be Subgraph of G; :: thesis: ( H is spanning implies not H is Dcomplete )
consider v, w being Vertex of G such that
A1: ( v <> w & ( for e being object holds not e DJoins v,w,G ) ) by Def1;
assume H is spanning ; :: thesis: not H is Dcomplete
then reconsider v9 = v, w9 = w as Vertex of H by GLIB_000:def 33;
take v9 ; :: according to GLIB_016:def 1 :: thesis: ex w being Vertex of H st
( v9 <> w & ( for e being object holds not e DJoins v9,w,H ) )
take w9 ; :: thesis: ( v9 <> w9 & ( for e being object holds not e DJoins v9,w9,H ) )
thus v9 <> w9 by A1; :: thesis: for e being object holds not e DJoins v9,w9,H
let e be object ; :: thesis: not e DJoins v9,w9,H
thus not e DJoins v9,w9,H by A1, GLIB_000:72; :: thesis: verum