let G be _Graph; :: thesis: for V being Subset of (the_Vertices_of G)
for H being addLoops of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) \/ (id V)
let V be Subset of (the_Vertices_of G); :: thesis: for H being addLoops of G,V holds VertexAdjSymRel H = (VertexAdjSymRel G) \/ (id V)
let H be addLoops of G,V; :: thesis: VertexAdjSymRel H = (VertexAdjSymRel G) \/ (id V)
set R = VertexDomRel G;
reconsider I = id V as Relation ;
thus VertexAdjSymRel H = ((VertexDomRel G) \/ I) \/ ((VertexDomRel H) ~) by Th30
.= ((VertexDomRel G) \/ I) \/ (((VertexDomRel G) \/ I) ~) by Th30
.= ((VertexDomRel G) \/ I) \/ (((VertexDomRel G) ~) \/ (I ~)) by RELAT_1:23
.= ((VertexDomRel G) \/ (((VertexDomRel G) ~) \/ I)) \/ I by XBOOLE_1:4
.= (((VertexDomRel G) \/ ((VertexDomRel G) ~)) \/ I) \/ I by XBOOLE_1:4
.= ((VertexDomRel G) \/ ((VertexDomRel G) ~)) \/ (I \/ I) by XBOOLE_1:4
.= (VertexAdjSymRel G) \/ (id V) ; :: thesis: verum