let G be _Graph; :: thesis: for V being set
for H being removeVertices of G,V st V c< the_Vertices_of G holds
VertexAdjSymRel H = (VertexAdjSymRel 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
VertexAdjSymRel H = (VertexAdjSymRel 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 VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) )
assume A1: V c< the_Vertices_of G ; :: thesis: VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:])
set V1 = [:V,(the_Vertices_of G):];
set V2 = [:(the_Vertices_of G),V:];
A2: VertexDomRel H = (VertexDomRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) by A1, Th22;
then (VertexDomRel H) ~ = ((VertexDomRel G) ~) \ (([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) ~) by RELAT_1:24
.= ((VertexDomRel G) ~) \ (([:V,(the_Vertices_of G):] ~) \/ ([:(the_Vertices_of G),V:] ~)) by RELAT_1:23
.= ((VertexDomRel G) ~) \ (([:V,(the_Vertices_of G):] ~) \/ [:V,(the_Vertices_of G):]) by SYSREL:5
.= ((VertexDomRel G) ~) \ ([:(the_Vertices_of G),V:] \/ [:V,(the_Vertices_of G):]) by SYSREL:5 ;
hence VertexAdjSymRel H = (VertexAdjSymRel G) \ ([:V,(the_Vertices_of G):] \/ [:(the_Vertices_of G),V:]) by A2, XBOOLE_1:42; :: thesis: verum