let G1 be _Graph; :: thesis:
let G2 be GraphComplement of G1; :: thesis:
let v1 be Vertex of G1; :: thesis:
let v2 be Vertex of G2; :: thesis:
assume A1: ( v1 = v2 & G1 .order() = 2 ) ; :: thesis:
then G2 .order() = 2 by Th111;
then consider u1, u2 being object such that
A2: ( u1 <> u2 & the_Vertices_of G2 = {u1,u2} ) by CARD_2:60;
A3: the_Vertices_of G1 = the_Vertices_of G2 by Th98;
then reconsider u1 = u1, u2 = u2 as Vertex of G1 by A2, TARSKI:def 2;

hereby :: thesis:

assume v1 is endvertex ; :: thesis:
then consider e1 being object such that
A4: ( v1 .edgesInOut() = {e1} & not e1 Joins v1,v1,G1 ) by GLIB_000:def 51;
e1 in v1 .edgesInOut() by A4, TARSKI:def 1;
then consider v9 being Vertex of G1 such that
A5: e1 Joins v1,v9,G1 by GLIB_000:64;
A6: v1 <> v9 by A4, A5;
v9 in the_Vertices_of G1 ;
then v9 in the_Vertices_of G2 by Th98;
then A7: ( v9 = u1 or v9 = u2 ) by A2, TARSKI:def 2;
assume not v2 is isolated ; :: thesis:
then v2 .edgesInOut() <> {} by GLIB_000:def 49;
then consider e2 being object such that
A8: e2 in v2 .edgesInOut() by XBOOLE_0:def 1;
consider u being Vertex of G2 such that
A9: e2 Joins v2,u,G2 by A8, GLIB_000:64;

per cases by A2, TARSKI:def 2;

suppose ( v2 = u1 & u = u1 ) ; :: thesis:

hence contradiction by A9, GLIB_000:18; :: thesis:

end;

suppose ( v2 = u1 & u = u2 ) ; :: thesis:

hence contradiction by A1, A5, A6, A7, A9, Th100; :: thesis:

end;

suppose ( v2 = u2 & u = u1 ) ; :: thesis:

hence contradiction by A1, A5, A6, A7, A9, Th100; :: thesis:

end;

suppose ( v2 = u2 & u = u2 ) ; :: thesis:

hence contradiction by A9, GLIB_000:18; :: thesis:

end;

end;

end;

assume A10: v1 is isolated ; :: thesis:

per cases by A2, A3, TARSKI:def 2;

suppose A11: v1 = u1 ; :: thesis:

for e1 being object holds not e1 Joins v1,u2,G1 by A10, GLIB_000:143;
then consider e2 being object such that
A12: e2 Joins v1,u2,G2 by A2, A11, Th98;
for e being object holds
( e in v2 .edgesInOut() iff e = e2 )

proof

let e be object ; :: thesis:

hereby :: thesis:

assume e in v2 .edgesInOut() ; :: thesis:
then consider v9 being Vertex of G2 such that
A13: e Joins v2,v9,G2 by GLIB_000:64;
v9 = u2

proof

assume v9 <> u2 ; :: thesis:
then v9 = u1 by A2, TARSKI:def 2;
hence contradiction by A1, A11, A13, GLIB_000:18; :: thesis:

end;

hence e = e2 by A1, A12, A13, GLIB_000:def 20; :: thesis:

end;

reconsider w = u2 as Vertex of G2 by A2, TARSKI:def 2;
assume e = e2 ; :: thesis:
then ( e Joins v2,w,G2 & e is set ) by A1, A12, TARSKI:1;
hence e in v2 .edgesInOut() by GLIB_000:64; :: thesis:

end;

then v2 .edgesInOut() = {e2} by TARSKI:def 1;
hence v2 is endvertex by GLIB_000:18, GLIB_000:def 51; :: thesis:

end;

suppose A14: v1 = u2 ; :: thesis:

for e1 being object holds not e1 Joins v1,u1,G1 by A10, GLIB_000:143;
then consider e2 being object such that
A15: e2 Joins v1,u1,G2 by A2, A14, Th98;
for e being object holds
( e in v2 .edgesInOut() iff e = e2 )

proof

let e be object ; :: thesis:

hereby :: thesis:

assume e in v2 .edgesInOut() ; :: thesis:
then consider v9 being Vertex of G2 such that
A16: e Joins v2,v9,G2 by GLIB_000:64;
v9 = u1

proof

assume v9 <> u1 ; :: thesis:
then v9 = u2 by A2, TARSKI:def 2;
hence contradiction by A1, A14, A16, GLIB_000:18; :: thesis:

end;

hence e = e2 by A1, A15, A16, GLIB_000:def 20; :: thesis:

end;

reconsider w = u1 as Vertex of G2 by A2, TARSKI:def 2;
assume e = e2 ; :: thesis:
then ( e Joins v2,w,G2 & e is set ) by A1, A15, TARSKI:1;
hence e in v2 .edgesInOut() by GLIB_000:64; :: thesis:

end;

then v2 .edgesInOut() = {e2} by TARSKI:def 1;
hence v2 is endvertex by GLIB_000:18, GLIB_000:def 51; :: thesis:

end;

end;