let G2 be _Graph; :: thesis: for E being set
for G1 being reverseEdgeDirections of G2,E
for v being set
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})
let E be set ; :: thesis: for G1 being reverseEdgeDirections of G2,E
for v being set
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})
let G1 be reverseEdgeDirections of G2,E; :: thesis: for v being set
for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})
let v be set ; :: thesis: for G3 being removeVertex of G1,v
for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})
let G3 be removeVertex of G1,v; :: thesis: for G4 being removeVertex of G2,v holds G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})
let G4 be removeVertex of G2,v; :: thesis: G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

per cases ( E c= the_Edges_of G2 or not E c= the_Edges_of G2 ) ;

suppose A1: E c= the_Edges_of G2 ; :: thesis: G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

then A2: ( the_Vertices_of G1 = the_Vertices_of G2 & the_Edges_of G1 = the_Edges_of G2 & the_Source_of G1 = (the_Source_of G2) +* ((the_Target_of G2) | E) & the_Target_of G1 = (the_Target_of G2) +* ((the_Source_of G2) | E) ) by Def1;
then A4: G1 .edgesBetween ((the_Vertices_of G1) \ {v}) = G2 .edgesBetween ((the_Vertices_of G2) \ {v}) by Th11;

per cases ( not v in the_Vertices_of G2 or v in the_Vertices_of G2 ) ;

suppose A5: not v in the_Vertices_of G2 ; :: thesis: G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

then ( (the_Vertices_of G1) \ {v} = the_Vertices_of G1 & (the_Vertices_of G2) \ {v} = the_Vertices_of G2 ) by A2, ZFMISC_1:57;
then A6: ( G1 == G3 & G2 == G4 ) by GLIB_000:94;
{v} /\ (the_Vertices_of G1) = {} by XBOOLE_0:def 7, A2, A5, ZFMISC_1:50;
then a7: G1 .edgesInOut {v} = {} by GLIB_000:103;
G3 is reverseEdgeDirections of G2,E by A6, Th2;
then G2 is reverseEdgeDirections of G3,E by Th3;
hence G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v}) by A6, a7, Th2; :: thesis: verum

end;

suppose A8: v in the_Vertices_of G2 ; :: thesis: G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

then A9: v in the_Vertices_of G1 by A2;

per cases ( not G2 is _trivial or G2 is _trivial ) ;

suppose A10: not G2 is _trivial ; :: thesis: G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

then A11: ( the_Vertices_of G4 = (the_Vertices_of G2) \ {v} & the_Edges_of G4 = G2 .edgesBetween ((the_Vertices_of G2) \ {v}) ) by A8, GLIB_000:47;
A12: ( the_Vertices_of G3 = (the_Vertices_of G1) \ {v} & the_Edges_of G3 = G1 .edgesBetween ((the_Vertices_of G1) \ {v}) ) by A2, A8, GLIB_000:47, A10;
then A13: ( the_Vertices_of G4 = the_Vertices_of G3 & the_Edges_of G4 = the_Edges_of G3 ) by A11, A2, A4;
A14: ( dom (the_Source_of G4) = the_Edges_of G4 & dom (the_Target_of G4) = the_Edges_of G4 ) by GLIB_000:4;
for e being object st e in E \ (G1 .edgesInOut {v}) holds
e in the_Edges_of G3

proof

let e be object ; :: thesis: ( e in E \ (G1 .edgesInOut {v}) implies e in the_Edges_of G3 )
assume e in E \ (G1 .edgesInOut {v}) ; :: thesis: e in the_Edges_of G3
then A15: ( e in E & not e in G1 .edgesInOut {v} ) by XBOOLE_0:def 5;
then A16: e in the_Edges_of G1 by A1, A2;
A17: ( not (the_Source_of G1) . e in {v} & not (the_Target_of G1) . e in {v} ) by A15, A1, A2, GLIB_000:28;
e Joins (the_Source_of G1) . e,(the_Target_of G1) . e,G1 by A1, A2, A15, GLIB_000:def 13;
then ( (the_Source_of G1) . e in the_Vertices_of G1 & (the_Target_of G1) . e in the_Vertices_of G1 ) by GLIB_000:13;
then ( (the_Source_of G1) . e in (the_Vertices_of G1) \ {v} & (the_Target_of G1) . e in (the_Vertices_of G1) \ {v} ) by A17, XBOOLE_0:def 5;
hence e in the_Edges_of G3 by A12, A16, GLIB_000:31; :: thesis: verum

end;

then A18: E \ (G1 .edgesInOut {v}) c= the_Edges_of G3 by TARSKI:def 3;
A19: for e being object st e in the_Edges_of G4 holds
not e in G1 .edgesInOut {v}

proof

let e be object ; :: thesis: ( e in the_Edges_of G4 implies not e in G1 .edgesInOut {v} )
assume e in the_Edges_of G4 ; :: thesis: not e in G1 .edgesInOut {v}
then A20: e in the_Edges_of G3 by A13;
assume e in G1 .edgesInOut {v} ; :: thesis: contradiction
then ( e in the_Edges_of G1 & ( (the_Source_of G1) . e in {v} or (the_Target_of G1) . e in {v} ) ) by GLIB_000:28;
then A21: ( (the_Source_of G3) . e in {v} or (the_Target_of G3) . e in {v} ) by A20, GLIB_000:def 32;
e Joins (the_Source_of G3) . e,(the_Target_of G3) . e,G3 by A20, GLIB_000:def 13;
then ( (the_Source_of G3) . e in the_Vertices_of G3 & (the_Target_of G3) . e in the_Vertices_of G3 ) by GLIB_000:13;
hence contradiction by A21, A12, XBOOLE_0:def 5; :: thesis: verum

end;

set S = (the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})));
A22: dom ((the_Target_of G3) | (E \ (G1 .edgesInOut {v}))) = (dom (the_Target_of G3)) /\ (E \ (G1 .edgesInOut {v})) by RELAT_1:61
.= (the_Edges_of G3) /\ (E \ (G1 .edgesInOut {v})) by GLIB_000:4 ;
A23: dom ((the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) = (dom (the_Source_of G3)) \/ (dom ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) by FUNCT_4:def 1
.= (the_Edges_of G3) \/ (dom ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) by GLIB_000:4
.= dom (the_Source_of G4) by A13, A14, A22, XBOOLE_1:22 ;
set T = (the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})));
A24: dom ((the_Source_of G3) | (E \ (G1 .edgesInOut {v}))) = (dom (the_Source_of G3)) /\ (E \ (G1 .edgesInOut {v})) by RELAT_1:61
.= (the_Edges_of G3) /\ (E \ (G1 .edgesInOut {v})) by GLIB_000:4 ;
A25: dom ((the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) = (dom (the_Target_of G3)) \/ (dom ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) by FUNCT_4:def 1
.= (the_Edges_of G3) \/ (dom ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) by GLIB_000:4
.= dom (the_Target_of G4) by A13, A14, A24, XBOOLE_1:22 ;
for e being object st e in dom (the_Source_of G4) holds
(the_Source_of G4) . e = ((the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) . e

proof

let e be object ; :: thesis: ( e in dom (the_Source_of G4) implies (the_Source_of G4) . e = ((the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) . e )
assume e in dom (the_Source_of G4) ; :: thesis: (the_Source_of G4) . e = ((the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) . e
then A26: e in the_Edges_of G4 ;

per cases ( e in E \ (G1 .edgesInOut {v}) or not e in E \ (G1 .edgesInOut {v}) ) ;

suppose A27: e in E \ (G1 .edgesInOut {v}) ; :: thesis: (the_Source_of G4) . e = ((the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) . e

then A28: e in E ;
A29: e in the_Edges_of G3 by A27, A18;
A30: e in dom ((the_Target_of G3) | (E \ (G1 .edgesInOut {v}))) by A27, A18, A22, XBOOLE_0:def 4;
e in the_Edges_of G2 by A26;
then e in dom (the_Source_of G2) by GLIB_000:4;
then e in (dom (the_Source_of G2)) /\ E by A28, XBOOLE_0:def 4;
then A31: e in dom ((the_Source_of G2) | E) by RELAT_1:61;
thus ((the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) . e = ((the_Target_of G3) | (E \ (G1 .edgesInOut {v}))) . e by A30, FUNCT_4:13
.= (the_Target_of G3) . e by A27, FUNCT_1:49
.= (the_Target_of G1) . e by A29, GLIB_000:def 32
.= ((the_Source_of G2) | E) . e by A2, A31, FUNCT_4:13
.= (the_Source_of G2) . e by A28, FUNCT_1:49
.= (the_Source_of G4) . e by A26, GLIB_000:def 32 ; :: thesis: verum

end;

suppose A32: not e in E \ (G1 .edgesInOut {v}) ; :: thesis: (the_Source_of G4) . e = ((the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) . e

not e in G1 .edgesInOut {v} by A26, A19;
then A33: not e in dom ((the_Target_of G2) | E) by A32, XBOOLE_0:def 5;
A34: not e in dom ((the_Target_of G3) | (E \ (G1 .edgesInOut {v}))) by A32;
thus ((the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v})))) . e = (the_Source_of G3) . e by A34, FUNCT_4:11
.= (the_Source_of G1) . e by A13, A26, GLIB_000:def 32
.= (the_Source_of G2) . e by A2, A33, FUNCT_4:11
.= (the_Source_of G4) . e by A26, GLIB_000:def 32 ; :: thesis: verum

end;

end;

end;

then A35: the_Source_of G4 = (the_Source_of G3) +* ((the_Target_of G3) | (E \ (G1 .edgesInOut {v}))) by A23, FUNCT_1:2;
for e being object st e in dom (the_Target_of G4) holds
(the_Target_of G4) . e = ((the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) . e

proof

let e be object ; :: thesis: ( e in dom (the_Target_of G4) implies (the_Target_of G4) . e = ((the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) . e )
assume e in dom (the_Target_of G4) ; :: thesis: (the_Target_of G4) . e = ((the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) . e
then A36: e in the_Edges_of G4 ;

per cases ( e in E \ (G1 .edgesInOut {v}) or not e in E \ (G1 .edgesInOut {v}) ) ;

suppose A37: e in E \ (G1 .edgesInOut {v}) ; :: thesis: (the_Target_of G4) . e = ((the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) . e

then A38: e in E ;
A39: e in the_Edges_of G3 by A37, A18;
A40: e in dom ((the_Source_of G3) | (E \ (G1 .edgesInOut {v}))) by A37, A18, A24, XBOOLE_0:def 4;
e in the_Edges_of G2 by A36;
then e in dom (the_Target_of G2) by GLIB_000:4;
then e in (dom (the_Target_of G2)) /\ E by A38, XBOOLE_0:def 4;
then A41: e in dom ((the_Target_of G2) | E) by RELAT_1:61;
thus ((the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) . e = ((the_Source_of G3) | (E \ (G1 .edgesInOut {v}))) . e by A40, FUNCT_4:13
.= (the_Source_of G3) . e by A37, FUNCT_1:49
.= (the_Source_of G1) . e by A39, GLIB_000:def 32
.= ((the_Target_of G2) | E) . e by A2, A41, FUNCT_4:13
.= (the_Target_of G2) . e by A38, FUNCT_1:49
.= (the_Target_of G4) . e by A36, GLIB_000:def 32 ; :: thesis: verum

end;

suppose A42: not e in E \ (G1 .edgesInOut {v}) ; :: thesis: (the_Target_of G4) . e = ((the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) . e

not e in G1 .edgesInOut {v} by A36, A19;
then A43: not e in dom ((the_Source_of G2) | E) by A42, XBOOLE_0:def 5;
not e in dom ((the_Source_of G3) | (E \ (G1 .edgesInOut {v}))) by A42;
hence ((the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v})))) . e = (the_Target_of G3) . e by FUNCT_4:11
.= (the_Target_of G1) . e by A13, A36, GLIB_000:def 32
.= (the_Target_of G2) . e by A2, A43, FUNCT_4:11
.= (the_Target_of G4) . e by A36, GLIB_000:def 32 ;
:: thesis: verum

end;

end;

end;

then the_Target_of G4 = (the_Target_of G3) +* ((the_Source_of G3) | (E \ (G1 .edgesInOut {v}))) by A25, FUNCT_1:2;
hence G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v}) by A13, A18, A35, Def1; :: thesis: verum

end;

suppose A45: G2 is _trivial ; :: thesis: G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

then consider v1 being Vertex of G1 such that
A47: the_Vertices_of G1 = {v1} by GLIB_000:22;
v = v1 by A9, A47, TARSKI:def 1;
then ( (the_Vertices_of G1) \ {v} is empty & (the_Vertices_of G2) \ {v} is empty ) by XBOOLE_1:37, A2, A47;
then A48: ( G1 == G3 & G2 == G4 ) by GLIB_000:def 37;
G3 is reverseEdgeDirections of G2,E by A48, Th2;
then G3 == G2 by A45, Th6;
hence G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v}) by Th6, A45, A48, GLIB_000:85; :: thesis: verum

end;

end;

end;

end;

end;

suppose A50: not E c= the_Edges_of G2 ; :: thesis: G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v})

then A51: G1 == G2 by Def1;
then A52: (the_Vertices_of G1) \ {v} = (the_Vertices_of G2) \ {v} by GLIB_000:def 34;
then A53: G1 .edgesBetween ((the_Vertices_of G1) \ {v}) = G2 .edgesBetween ((the_Vertices_of G2) \ {v}) by A51, GLIB_000:90;
A54: not E \ (G1 .edgesInOut {v}) c= the_Edges_of G3

proof

assume E \ (G1 .edgesInOut {v}) c= the_Edges_of G3 ; :: thesis: contradiction
then E \ (G1 .edgesInOut {v}) c= the_Edges_of G1 by XBOOLE_1:1;
then (E \ (G1 .edgesInOut {v})) \/ (G1 .edgesInOut {v}) c= the_Edges_of G1 by XBOOLE_1:8;
then A55: E \/ (G1 .edgesInOut {v}) c= the_Edges_of G1 by XBOOLE_1:39;
not E c= the_Edges_of G1 by A50, A51, GLIB_000:def 34;
hence contradiction by A55, XBOOLE_1:11; :: thesis: verum

end;

G4 is removeVertex of G1,v by A51, A52, A53, GLIB_000:95;
then G3 == G4 by GLIB_000:93;
hence G4 is reverseEdgeDirections of G3,E \ (G1 .edgesInOut {v}) by A54, Def1; :: thesis: verum

end;

end;