let G1 be _Graph; :: thesis: for G2 being GraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & 4 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex
let G2 be GraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & 4 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 & 4 c= G1 .order() & v1 is endvertex holds
not v2 is endvertex
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & 4 c= G1 .order() & v1 is endvertex implies not v2 is endvertex )
assume A1: ( v1 = v2 & 4 c= G1 .order() ) ; :: thesis: ( not v1 is endvertex or not v2 is endvertex )
assume v1 is endvertex ; :: thesis: not v2 is endvertex
then consider x, y, z being Vertex of G1 such that
A2: ( v1 <> x & v1 <> y & v1 <> z & x <> y & x <> z & y <> z ) and
A3: ( v1,x are_adjacent & not v1,y are_adjacent & not v1,z are_adjacent ) by A1, GLIBPRE0:96;
reconsider u = y, w = z as Vertex of G2 by Th99;
( v2,u are_adjacent & v2,w are_adjacent ) by A1, A2, A3, Th99;
hence not v2 is endvertex by A2, GLIBPRE0:94; :: thesis: verum