let G1 be _Graph; :: thesis: for G2 being DLGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) )
let G2 be DLGraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 holds
( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 implies ( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) ) )
assume A1: v1 = v2 ; :: thesis: ( ( v1 is isolated implies not v2 is isolated ) & ( v1 is endvertex implies not v2 is endvertex ) )

hereby :: thesis: ( v1 is endvertex implies not v2 is endvertex )

assume A2: v1 is isolated ; :: thesis: not v2 is isolated
for e1 being object holds not e1 DJoins v1,v1,G1

proof

given e1 being object such that A3: e1 DJoins v1,v1,G1 ; :: thesis: contradiction
e1 Joins v1,v1,G1 by A3, GLIB_000:16;
hence contradiction by A2, GLIB_000:143; :: thesis: verum

end;

then consider e2 being object such that
A4: e2 DJoins v1,v1,G2 by Def6;
e2 Joins v2,v2,G2 by A1, A4, GLIB_000:16;
hence not v2 is isolated by GLIB_000:143; :: thesis: verum

end;

hereby :: thesis: verum

assume A5: v1 is endvertex ; :: thesis: not v2 is endvertex
for e1 being object holds not e1 DJoins v1,v1,G1

proof

given e1 being object such that A6: e1 DJoins v1,v1,G1 ; :: thesis: contradiction
e1 Joins v1,v1,G1 by A6, GLIB_000:16;
hence contradiction by A5, GLIB_000:146; :: thesis: verum

end;

then consider e2 being object such that
A7: e2 DJoins v1,v1,G2 by Def6;
e2 Joins v2,v2,G2 by A1, A7, GLIB_000:16;
hence not v2 is endvertex by GLIB_000:146; :: thesis: verum

end;