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 [b1,b2] in VertexAdjSymRel H ) )
hereby :: thesis: ( [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] implies [b1,b2] 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 not e in the_Edges_of G ; :: thesis: [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:]
end;
end;
end;
assume [v1,v2] in ((VertexAdjSymRel G) \/ [:{v},V:]) \/ [:V,{v}:] ; :: thesis: [b1,b2] 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 [v1,v2] in [:{v},V:] ; :: thesis: [b1,b2] 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: [b1,b2] 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