let G1 be _Graph; :: thesis: for G2 being LGraphComplement 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 LGraphComplement 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 v1 is isolated ; :: thesis: not v2 is isolated
then for e1 being object holds not e1 Joins v1,v1,G1 by GLIB_000:143;
then consider e2 being object such that
A2: e2 Joins v1,v1,G2 by Def7;
thus not v2 is isolated by A1, A2, GLIB_000:143; :: thesis: verum

end;

hereby :: thesis: verum

assume v1 is endvertex ; :: thesis: not v2 is endvertex
then for e1 being object holds not e1 Joins v1,v1,G1 by GLIB_000:146;
then consider e2 being object such that
A3: e2 Joins v1,v1,G2 by Def7;
thus not v2 is endvertex by A1, A3, GLIB_000:146; :: thesis: verum

end;