let G be _Graph; :: thesis: for H being DLGraphComplement of G holds VertexDomRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G)
let H be DLGraphComplement of G; :: thesis: VertexDomRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G)
set N = [:(the_Vertices_of G),(the_Vertices_of G):];
now :: thesis: for x, y being object holds
( ( [x,y] in VertexDomRel H implies [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G) ) & ( [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G) implies [x,y] in VertexDomRel H ) )
let x, y be object ; :: thesis: ( ( [x,y] in VertexDomRel H implies [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G) ) & ( [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G) implies [x,y] in VertexDomRel H ) )
hereby :: thesis: ( [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G) implies [x,y] in VertexDomRel H )
assume A1: [x,y] in VertexDomRel H ; :: thesis: [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G)
the_Vertices_of G = the_Vertices_of H by GLIB_012:def 6;
then A2: [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] by A1;
consider e2 being object such that
A3: e2 DJoins x,y,H by A1, Th1;
( x in the_Vertices_of G & y in the_Vertices_of G ) by A2, ZFMISC_1:87;
then for e1 being object holds not e1 DJoins x,y,G by A3, GLIB_012:def 6;
then not [x,y] in VertexDomRel G by Th1;
hence [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G) by A2, XBOOLE_0:def 5; :: thesis: verum
end;
assume [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G) ; :: thesis: [x,y] in VertexDomRel H
then A4: ( [x,y] in [:(the_Vertices_of G),(the_Vertices_of G):] & not [x,y] in VertexDomRel G ) by XBOOLE_0:def 5;
then A5: ( x in the_Vertices_of G & y in the_Vertices_of G ) by ZFMISC_1:87;
for e1 being object holds not e1 DJoins x,y,G by A4, Th1;
then ex e2 being object st e2 DJoins x,y,H by A5, GLIB_012:def 6;
hence [x,y] in VertexDomRel H by Th1; :: thesis: verum
end;
hence VertexDomRel H = [:(the_Vertices_of G),(the_Vertices_of G):] \ (VertexDomRel G) by RELAT_1:def 2; :: thesis: verum