let G be non _trivial _Graph; :: thesis:
let v be Vertex of G; :: thesis:
let H be removeVertex of G,v; :: thesis:
assume A1: v is isolated ; :: thesis:
set V1 = [:{v},(the_Vertices_of G):];
set V2 = [:(the_Vertices_of G),{v}:];
([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:]) /\ (VertexDomRel G) = {}

assume ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:]) /\ (VertexDomRel G) <> {} ; :: thesis:
then consider z being object such that
A2: z in ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:]) /\ (VertexDomRel G) by XBOOLE_0:def 1;
consider u, w being object such that
A3: z = [u,w] by A2, RELAT_1:def 1;
A4: ( [u,w] in [:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:] & [u,w] in VertexDomRel G ) by A2, A3, XBOOLE_0:def 4;
then consider e being object such that
A5: e DJoins u,w,G by Th1;

per cases in [:{v},(the_Vertices_of G):] or [u,w] in [:(the_Vertices_of G),{v}:] ) by A4, XBOOLE_0:def 3;

suppose [u,w] in [:{v},(the_Vertices_of G):] ; :: thesis:

then u in {v} by ZFMISC_1:87;
then u = v by TARSKI:def 1;
hence contradiction by A1, A5, GLIBPRE0:22; :: thesis:

end;

suppose [u,w] in [:(the_Vertices_of G),{v}:] ; :: thesis:

then w in {v} by ZFMISC_1:87;
then w = v by TARSKI:def 1;
hence contradiction by A1, A5, GLIBPRE0:22; :: thesis:

end;

end;

end;

then VertexDomRel G = (VertexDomRel G) \ ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:]) by XBOOLE_1:83, XBOOLE_0:def 7;
hence VertexDomRel H = VertexDomRel G by Th23; :: thesis: