let G be _Graph; :: thesis: for v being object
for V being Subset of (the_Vertices_of G)
for H being addAdjVertexAll of G,v,V st not v in the_Vertices_of G holds
VertexAdjSymRel H = ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]
let v be object ; :: thesis: for V being Subset of (the_Vertices_of G)
for H being addAdjVertexAll of G,v,V st not v in the_Vertices_of G holds
VertexAdjSymRel H = ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]
let V be Subset of (the_Vertices_of G); :: thesis: for H being addAdjVertexAll of G,v,V st not v in the_Vertices_of G holds
VertexAdjSymRel H = ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]
let H be addAdjVertexAll of G,v,V; :: thesis: ( not v in the_Vertices_of G implies VertexAdjSymRel H = ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] )
assume A1: not v in the_Vertices_of G ; :: thesis: VertexAdjSymRel H = ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]
then consider E being set such that
A2: ( card V = card E & E misses the_Edges_of G ) and
A3: the_Edges_of H = (the_Edges_of G) \/ E and
A4: for v1 being object st v1 in V holds
ex e1 being object st
( e1 in E & e1 Joins v1,v,H & ( for e2 being object st e2 Joins v1,v,H holds
e1 = e2 ) ) by GLIB_007:def 4;
set F = [:{v},V:];
set L = [:V,{v}:];

now :: thesis: for v1, v2 being object holds
( ( [v1,v2] in VertexAdjSymRel H implies [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] ) & ( [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] implies [v1,v2] in VertexAdjSymRel H ) )

let v1, v2 be object ; :: thesis: ( ( [v1,v2] in VertexAdjSymRel H implies [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] ) & ( [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] implies [b₁,b₂] in VertexAdjSymRel H ) )

hereby :: thesis: ( [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] implies [b₁,b₂] in VertexAdjSymRel H )

assume [v1,v2] in VertexAdjSymRel H ; :: thesis: [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]
then consider e being object such that
A5: e Joins v1,v2,H by Th32;

per cases ( e Joins v1,v2,G or not e in the_Edges_of G ) by A5, GLIB_006:72;

suppose e Joins v1,v2,G ; :: thesis: [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]

then [v1,v2] in VertexAdjSymRel G by Th32;
then [v1,v2] in (VertexAdjSymRel G) \/ [:{v},V:] by XBOOLE_0:def 3;
hence [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] by XBOOLE_0:def 3; :: thesis: verum

end;

suppose not e in the_Edges_of G ; :: thesis: [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]

per cases then ( ( v1 = v & v2 in V ) or ( v2 = v & v1 in V ) ) by A1, A2, A3, A5, GLIB_007:51;

suppose ( v1 = v & v2 in V ) ; :: thesis: [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]

then ( v1 in {v} & v2 in V ) by TARSKI:def 1;
then [v1,v2] in [:{v},V:] by ZFMISC_1:87;
then [v1,v2] in (VertexAdjSymRel G) \/ [:{v},V:] by XBOOLE_0:def 3;
hence [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] by XBOOLE_0:def 3; :: thesis: verum

end;

suppose ( v2 = v & v1 in V ) ; :: thesis: [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]

then ( v2 in {v} & v1 in V ) by TARSKI:def 1;
then [v1,v2] in [:V,{v}:] by ZFMISC_1:87;
hence [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

end;

end;

assume [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] ; :: thesis: [b₁,b₂] in VertexAdjSymRel H
then ( [v1,v2] in (VertexAdjSymRel G) \/ [:{v},V:] or [v1,v2] in [:V,{v}:] ) by XBOOLE_0:def 3;

per cases then ( [v1,v2] in VertexAdjSymRel G or [v1,v2] in [:{v},V:] or [v1,v2] in [:V,{v}:] ) by XBOOLE_0:def 3;

suppose A6: [v1,v2] in VertexAdjSymRel G ; :: thesis: [b₁,b₂] in VertexAdjSymRel H

G is Subgraph of H by GLIB_006:57;
hence [v1,v2] in VertexAdjSymRel H by A6, Th45, TARSKI:def 3; :: thesis: verum

end;

suppose [v1,v2] in [:{v},V:] ; :: thesis: [b₁,b₂] in VertexAdjSymRel H

then A7: ( v1 in {v} & v2 in V ) by ZFMISC_1:87;
then consider e1 being object such that
A8: ( e1 in E & e1 Joins v2,v,H ) and
for e2 being object st e2 Joins v2,v,H holds
e1 = e2 by A4;
e1 Joins v2,v1,H by A7, A8, TARSKI:def 1;
then e1 Joins v1,v2,H by GLIB_000:14;
hence [v1,v2] in VertexAdjSymRel H by Th32; :: thesis: verum

end;

suppose [v1,v2] in [:V,{v}:] ; :: thesis: [b₁,b₂] in VertexAdjSymRel H

then A9: ( v2 in {v} & v1 in V ) by ZFMISC_1:87;
then consider e1 being object such that
A10: ( e1 in E & e1 Joins v1,v,H ) and
for e2 being object st e2 Joins v1,v,H holds
e1 = e2 by A4;
e1 Joins v1,v2,H by A9, A10, TARSKI:def 1;
hence [v1,v2] in VertexAdjSymRel H by Th32; :: thesis: verum

end;

end;

end;

hence VertexAdjSymRel H = ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] by RELAT_1:def 2; :: thesis: verum