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 & v1 is isolated holds
v2 .allNeighbors() = the_Vertices_of G2
let G2 be LGraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
v2 .allNeighbors() = the_Vertices_of G2
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
v2 .allNeighbors() = the_Vertices_of G2
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & v1 is isolated implies v2 .allNeighbors() = the_Vertices_of G2 )
assume A1: ( v1 = v2 & v1 is isolated ) ; :: thesis: v2 .allNeighbors() = the_Vertices_of G2
then v1 .allNeighbors() = {} by GLIB_000:113;
hence v2 .allNeighbors() = (the_Vertices_of G2) \ {} by A1, Th77
.= the_Vertices_of G2 ;
:: thesis: verum