let G be non _trivial _Graph; :: thesis: for v being Vertex of G
for H being removeVertex of G,v st v is isolated holds
VertexDomRel H = VertexDomRel G
let v be Vertex of G; :: thesis: for H being removeVertex of G,v st v is isolated holds
VertexDomRel H = VertexDomRel G
let H be removeVertex of G,v; :: thesis: ( v is isolated implies VertexDomRel H = VertexDomRel G )
assume A1: v is isolated ; :: thesis: VertexDomRel H = VertexDomRel G
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) = {}

proof

assume ([:{v},(the_Vertices_of G):] \/ [:(the_Vertices_of G),{v}:]) /\ (VertexDomRel G) <> {} ; :: thesis: contradiction
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 ( [u,w] 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: contradiction

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

end;

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

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

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: verum