let G1 be _Graph; :: thesis: for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & 3 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex
let G2 be DGraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & 3 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & 3 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & 3 c= G1 .order() & v1 is endvertex implies not v2 is endvertex )
assume A1: ( v1 = v2 & 3 c= G1 .order() ) ; :: thesis: ( not v1 is endvertex or not v2 is endvertex )
assume v1 is endvertex ; :: thesis: not v2 is endvertex
then consider u, w being Vertex of G1 such that
A2: ( u <> v1 & w <> v1 & u <> w & u,v1 are_adjacent & not v1,w are_adjacent ) by A1, GLIBPRE0:95;
for e being object holds not e DJoins v1,w,G1

proof

given e being object such that A3: e DJoins v1,w,G1 ; :: thesis: contradiction
e Joins v1,w,G1 by A3, GLIB_000:16;
hence contradiction by A2, CHORD:def 3; :: thesis: verum

end;

then consider e1 being object such that
A4: e1 DJoins v1,w,G2 by A2, Th80;
for e being object holds not e DJoins w,v1,G1

proof

given e being object such that A5: e DJoins w,v1,G1 ; :: thesis: contradiction
e Joins v1,w,G1 by A5, GLIB_000:16;
hence contradiction by A2, CHORD:def 3; :: thesis: verum

end;

then consider e2 being object such that
A6: e2 DJoins w,v1,G2 by A2, Th80;
A7: e1 <> e2 by A2, A4, A6, GLIB_000:125;
reconsider w = w as Vertex of G2 by Th80;
reconsider e1 = e1, e2 = e2 as set by TARSKI:1;
( e1 Joins v2,w,G2 & e2 Joins v2,w,G2 ) by A1, A4, A6, GLIB_000:16;
then ( e1 in v2 .edgesInOut() & e2 in v2 .edgesInOut() ) by GLIB_000:64;
then A8: {e1,e2} c= v2 .edgesInOut() by ZFMISC_1:32;
assume v2 is endvertex ; :: thesis: contradiction
then consider e9 being object such that
A9: ( v2 .edgesInOut() = {e9} & not e9 Joins v2,v2,G2 ) by GLIB_000:def 51;
( e1 = e9 & e2 = e9 ) by A8, A9, ZFMISC_1:20;
hence contradiction by A7; :: thesis: verum