let G1 be _Graph; :: thesis: for G2 being DGraphComplement of G1
for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .outNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .allNeighbors() = (the_Vertices_of G2) \ {v2} )
let G2 be DGraphComplement of G1; :: thesis: for v1 being Vertex of G1
for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .outNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .allNeighbors() = (the_Vertices_of G2) \ {v2} )
let v1 be Vertex of G1; :: thesis: for v2 being Vertex of G2 st v1 = v2 & v1 is isolated holds
( v2 .inNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .outNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .allNeighbors() = (the_Vertices_of G2) \ {v2} )
let v2 be Vertex of G2; :: thesis: ( v1 = v2 & v1 is isolated implies ( v2 .inNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .outNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .allNeighbors() = (the_Vertices_of G2) \ {v2} ) )
assume A1: ( v1 = v2 & v1 is isolated ) ; :: thesis: ( v2 .inNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .outNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .allNeighbors() = (the_Vertices_of G2) \ {v2} )
then v1 .allNeighbors() = {} by GLIB_000:113;
then A2: ( v1 .inNeighbors() = {} & v1 .outNeighbors() = {} ) ;
thus A3: v2 .inNeighbors() = (the_Vertices_of G2) \ ({} \/ {v2}) by A1, A2, Th95
.= (the_Vertices_of G2) \ {v2} ; :: thesis: ( v2 .outNeighbors() = (the_Vertices_of G2) \ {v2} & v2 .allNeighbors() = (the_Vertices_of G2) \ {v2} )
thus v2 .outNeighbors() = (the_Vertices_of G2) \ ({} \/ {v2}) by A1, A2, Th95
.= (the_Vertices_of G2) \ {v2} ; :: thesis: v2 .allNeighbors() = (the_Vertices_of G2) \ {v2}
hence v2 .allNeighbors() = (the_Vertices_of G2) \ {v2} by A3; :: thesis: verum