let G1 be non _trivial _Graph; :: thesis: for v being Vertex of G1
for e being object
for G2 being removeVertex of G1,v st {e} = v .edgesInOut() & not e Joins v,v,G1 & G1 is not addAdjVertex of G2,v .adj e,e,v holds
G1 is addAdjVertex of G2,v,e,v .adj e
let v be Vertex of G1; :: thesis: for e being object
for G2 being removeVertex of G1,v st {e} = v .edgesInOut() & not e Joins v,v,G1 & G1 is not addAdjVertex of G2,v .adj e,e,v holds
G1 is addAdjVertex of G2,v,e,v .adj e
let e be object ; :: thesis: for G2 being removeVertex of G1,v st {e} = v .edgesInOut() & not e Joins v,v,G1 & G1 is not addAdjVertex of G2,v .adj e,e,v holds
G1 is addAdjVertex of G2,v,e,v .adj e
let G2 be removeVertex of G1,v; :: thesis: ( {e} = v .edgesInOut() & not e Joins v,v,G1 & G1 is not addAdjVertex of G2,v .adj e,e,v implies G1 is addAdjVertex of G2,v,e,v .adj e )
assume A1: ( {e} = v .edgesInOut() & not e Joins v,v,G1 ) ; :: thesis: ( G1 is addAdjVertex of G2,v .adj e,e,v or G1 is addAdjVertex of G2,v,e,v .adj e )
A2: G1 is Supergraph of G2 by GLIB_006:57;
A3: the_Vertices_of G1 = ((the_Vertices_of G1) \ {v}) \/ {v} by ZFMISC_1:116
.= (the_Vertices_of G2) \/ {v} by GLIB_000:47 ;
A4: e in {e} by TARSKI:def 1;
A5: the_Edges_of G1 = ((the_Edges_of G1) \ {e}) \/ {e} by A1, A4, ZFMISC_1:116
.= ((G1 .edgesBetween (the_Vertices_of G1)) \ (v .edgesInOut())) \/ {e} by A1, GLIB_000:34
.= (G1 .edgesBetween ((the_Vertices_of G1) \ {v})) \/ {e} by GLIB_000:107
.= (the_Edges_of G2) \/ {e} by GLIB_000:47 ;
set u = (the_Source_of G1) . e;
set w = (the_Target_of G1) . e;
v in {v} by TARSKI:def 1;
then not v in (the_Vertices_of G1) \ {v} by XBOOLE_0:def 5;
then A6: not v in the_Vertices_of G2 by GLIB_000:47;
not e in (G1 .edgesBetween (the_Vertices_of G1)) \ (v .edgesInOut()) by A1, A4, XBOOLE_0:def 5;
then not e in G1 .edgesBetween ((the_Vertices_of G1) \ {v}) by GLIB_000:107;
then A7: not e in the_Edges_of G2 by GLIB_000:47;
e in v .edgesInOut() by A1, TARSKI:def 1;
then A8: v <> v .adj e by A1, GLIB_000:67;
then not v .adj e in {v} by TARSKI:def 1;
then v .adj e in (the_Vertices_of G1) \ {v} by XBOOLE_0:def 5;
then A9: v .adj e in the_Vertices_of G2 by GLIB_000:47;
A10: dom (the_Source_of G1) = the_Edges_of G1 by FUNCT_2:def 1
.= (dom (the_Source_of G2)) \/ {e} by A5, FUNCT_2:def 1 ;
A11: dom (the_Target_of G1) = the_Edges_of G1 by FUNCT_2:def 1
.= (dom (the_Target_of G2)) \/ {e} by A5, FUNCT_2:def 1 ;
e in v .edgesInOut() by A1, TARSKI:def 1;

per cases then ( (the_Source_of G1) . e = v or (the_Target_of G1) . e = v ) by GLIB_000:61;

suppose A12: (the_Source_of G1) . e = v ; :: thesis: ( G1 is addAdjVertex of G2,v .adj e,e,v or G1 is addAdjVertex of G2,v,e,v .adj e )

then A13: (the_Target_of G1) . e = v .adj e by A1, A4, A8, GLIB_000:def 41;
A14: dom (the_Source_of G1) = (dom (the_Source_of G2)) \/ (dom ({e} --> v)) by A10
.= dom ((the_Source_of G2) +* ({e} --> v)) by FUNCT_4:def 1
.= dom ((the_Source_of G2) +* (e .--> v)) by FUNCOP_1:def 9 ;
for e0 being object st e0 in dom (the_Source_of G1) holds
(the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> v)) . e0

proof

let e0 be object ; :: thesis: ( e0 in dom (the_Source_of G1) implies (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> v)) . e0 )
assume A15: e0 in dom (the_Source_of G1) ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> v)) . e0

per cases ( e0 = e or e0 <> e ) ;

suppose e0 = e ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> v)) . e0

hence (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> v)) . e0 by A12, FUNCT_4:113; :: thesis: verum

end;

suppose A16: e0 <> e ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> v)) . e0

then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G2 by A5, A15, XBOOLE_0:def 3;
hence (the_Source_of G1) . e0 = (the_Source_of G2) . e0 by GLIB_000:def 32
.= ((the_Source_of G2) +* (e .--> v)) . e0 by A16, FUNCT_4:83 ;
:: thesis: verum

end;

end;

end;

then A17: the_Source_of G1 = (the_Source_of G2) +* (e .--> v) by A14, FUNCT_1:2;
A18: dom (the_Target_of G1) = (dom (the_Target_of G2)) \/ (dom ({e} --> (v .adj e))) by A11
.= dom ((the_Target_of G2) +* ({e} --> (v .adj e))) by FUNCT_4:def 1
.= dom ((the_Target_of G2) +* (e .--> (v .adj e))) by FUNCOP_1:def 9 ;
for e0 being object st e0 in dom (the_Target_of G1) holds
(the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> (v .adj e))) . e0

proof

let e0 be object ; :: thesis: ( e0 in dom (the_Target_of G1) implies (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> (v .adj e))) . e0 )
assume A19: e0 in dom (the_Target_of G1) ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> (v .adj e))) . e0

per cases ( e0 = e or e0 <> e ) ;

suppose e0 = e ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> (v .adj e))) . e0

hence (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> (v .adj e))) . e0 by A13, FUNCT_4:113; :: thesis: verum

end;

suppose A20: e0 <> e ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> (v .adj e))) . e0

then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G2 by A5, A19, XBOOLE_0:def 3;
hence (the_Target_of G1) . e0 = (the_Target_of G2) . e0 by GLIB_000:def 32
.= ((the_Target_of G2) +* (e .--> (v .adj e))) . e0 by A20, FUNCT_4:83 ;
:: thesis: verum

end;

end;

end;

then the_Target_of G1 = (the_Target_of G2) +* (e .--> (v .adj e)) by A18, FUNCT_1:2;
hence ( G1 is addAdjVertex of G2,v .adj e,e,v or G1 is addAdjVertex of G2,v,e,v .adj e ) by A2, A3, A5, A6, A7, A9, A17, GLIB_006:def 12; :: thesis: verum

end;

suppose A21: (the_Target_of G1) . e = v ; :: thesis: ( G1 is addAdjVertex of G2,v .adj e,e,v or G1 is addAdjVertex of G2,v,e,v .adj e )

then A22: (the_Source_of G1) . e = v .adj e by A1, A4, GLIB_000:def 41;
A23: dom (the_Target_of G1) = (dom (the_Target_of G2)) \/ (dom ({e} --> v)) by A11
.= dom ((the_Target_of G2) +* ({e} --> v)) by FUNCT_4:def 1
.= dom ((the_Target_of G2) +* (e .--> v)) by FUNCOP_1:def 9 ;
for e0 being object st e0 in dom (the_Target_of G1) holds
(the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> v)) . e0

proof

let e0 be object ; :: thesis: ( e0 in dom (the_Target_of G1) implies (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> v)) . e0 )
assume A24: e0 in dom (the_Target_of G1) ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> v)) . e0

per cases ( e0 = e or e0 <> e ) ;

suppose e0 = e ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> v)) . e0

hence (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> v)) . e0 by A21, FUNCT_4:113; :: thesis: verum

end;

suppose A25: e0 <> e ; :: thesis: (the_Target_of G1) . e0 = ((the_Target_of G2) +* (e .--> v)) . e0

then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G2 by A5, A24, XBOOLE_0:def 3;
hence (the_Target_of G1) . e0 = (the_Target_of G2) . e0 by GLIB_000:def 32
.= ((the_Target_of G2) +* (e .--> v)) . e0 by A25, FUNCT_4:83 ;
:: thesis: verum

end;

end;

end;

then A26: the_Target_of G1 = (the_Target_of G2) +* (e .--> v) by A23, FUNCT_1:2;
A27: dom (the_Source_of G1) = (dom (the_Source_of G2)) \/ (dom ({e} --> (v .adj e))) by A10
.= dom ((the_Source_of G2) +* ({e} --> (v .adj e))) by FUNCT_4:def 1
.= dom ((the_Source_of G2) +* (e .--> (v .adj e))) by FUNCOP_1:def 9 ;
for e0 being object st e0 in dom (the_Source_of G1) holds
(the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> (v .adj e))) . e0

proof

let e0 be object ; :: thesis: ( e0 in dom (the_Source_of G1) implies (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> (v .adj e))) . e0 )
assume A28: e0 in dom (the_Source_of G1) ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> (v .adj e))) . e0

per cases ( e0 = e or e0 <> e ) ;

suppose e0 = e ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> (v .adj e))) . e0

hence (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> (v .adj e))) . e0 by A22, FUNCT_4:113; :: thesis: verum

end;

suppose A29: e0 <> e ; :: thesis: (the_Source_of G1) . e0 = ((the_Source_of G2) +* (e .--> (v .adj e))) . e0

then not e0 in {e} by TARSKI:def 1;
then e0 in the_Edges_of G2 by A5, A28, XBOOLE_0:def 3;
hence (the_Source_of G1) . e0 = (the_Source_of G2) . e0 by GLIB_000:def 32
.= ((the_Source_of G2) +* (e .--> (v .adj e))) . e0 by A29, FUNCT_4:83 ;
:: thesis: verum

end;

end;

end;

then the_Source_of G1 = (the_Source_of G2) +* (e .--> (v .adj e)) by A27, FUNCT_1:2;
hence ( G1 is addAdjVertex of G2,v .adj e,e,v or G1 is addAdjVertex of G2,v,e,v .adj e ) by A2, A3, A5, A6, A7, A9, A26, GLIB_006:def 12; :: thesis: verum

end;

end;