let G be _Graph; :: thesis: for V being set
for H being removeVertices of G,V st V c< the_Vertices_of G holds
VertexDomRel H = (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:])
let V be set ; :: thesis: for H being removeVertices of G,V st V c< the_Vertices_of G holds
VertexDomRel H = (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:])
let H be removeVertices of G,V; :: thesis: ( V c< the_Vertices_of G implies VertexDomRel H = (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) )
assume V c< the_Vertices_of G ; :: thesis: VertexDomRel H = (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:])
then A1: ( the_Vertices_of H = (the_Vertices_of G) \ V & the_Edges_of H = G .edgesBetween ((the_Vertices_of G) \ V) ) by GLIB_000:49;
now :: thesis: for v, w being object holds
( ( [v,w] in VertexDomRel H implies [v,w] in (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) ) & ( [v,w] in (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) implies [v,w] in VertexDomRel H ) )
let v, w be object ; :: thesis: ( ( [v,w] in VertexDomRel H implies [v,w] in (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) ) & ( [v,w] in (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) implies [v,w] in VertexDomRel H ) )
hereby :: thesis: ( [v,w] in (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) implies [v,w] in VertexDomRel H )
assume A2: [v,w] in VertexDomRel H ; :: thesis: [v,w] in (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:])
then A3: [v,w] in VertexDomRel G by Th15, TARSKI:def 3;
consider e being object such that
A4: e DJoins v,w,H by A2, Th1;
e Joins v,w,H by A4, GLIB_000:16;
then ( v in the_Vertices_of H & w in the_Vertices_of H ) by GLIB_000:13;
then ( not v in V & not w in V ) by A1, XBOOLE_0:def 5;
then ( not [v,w] in [:V,(the_Vertices_of G):] & not [v,w] in [:(the_Vertices_of G),V:] ) by ZFMISC_1:87;
then not [v,w] in [:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:] by XBOOLE_0:def 3;
hence [v,w] in (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) by A3, XBOOLE_0:def 5; :: thesis: verum
end;
assume [v,w] in (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) ; :: thesis: [v,w] in VertexDomRel H
then A5: ( [v,w] in VertexDomRel G & not [v,w] in [:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:] ) by XBOOLE_0:def 5;
then A6: ( not [v,w] in [:V,(the_Vertices_of G):] & not [v,w] in [:(the_Vertices_of G),V:] ) by XBOOLE_0:def 3;
consider e being object such that
A7: e DJoins v,w,G by A5, Th1;
A8: e Joins v,w,G by A7, GLIB_000:16;
then A9: ( v in the_Vertices_of G & w in the_Vertices_of G ) by GLIB_000:13;
then ( not v in V & not w in V ) by A6, ZFMISC_1:87;
then ( v in (the_Vertices_of G) \ V & w in (the_Vertices_of G) \ V ) by A9, XBOOLE_0:def 5;
then A10: e in the_Edges_of H by A1, A8, GLIB_000:32;
( e is set & v is set & w is set ) by TARSKI:1;
then e DJoins v,w,H by A7, A10, GLIB_000:73;
hence [v,w] in VertexDomRel H by Th1; :: thesis: verum
end;
hence VertexDomRel H = (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) by RELAT_1:def 2; :: thesis: verum