set E = { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ;
deffunc H₁( object ) -> Element of Segm ($1 `2) = the Element of Segm ($1 `2);
consider s being Function such that
A1: ( dom s = { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } & ( for x being object st x in { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } holds
s . x = H₁(x) ) ) from FUNCT_1:sch 3();

now :: thesis: for y being object st y in rng s holds
y in the_Vertices_of G

let y be object ; :: thesis: ( y in rng s implies y in the_Vertices_of G )
assume y in rng s ; :: thesis: y in the_Vertices_of G
then consider x being object such that
A2: ( x in dom s & s . x = y ) by FUNCT_1:def 3;
consider v, w being Vertex of G such that
A3: x = [(the_Edges_of G),{v,w}] and
for e being object holds not e Joins v,w,G by A1, A2;
y = H₁(x) by A1, A2
.= the Element of {v,w} by A3 ;
hence y in the_Vertices_of G ; :: thesis: verum

end;

then reconsider s = s as Function of { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,(the_Vertices_of G) by A1, TARSKI:def 3, FUNCT_2:2;
deffunc H₂( object ) -> set = IFEQ (((Segm ($1 `2)) \ {H<sub>1</sub>($1)}),{},H<sub>1</sub>($1), the Element of (Segm ($1 `2)) \ {H₁($1)});
A4: for x, y being object st x <> y holds
H₂([(the_Edges_of G),{x,y}]) = the Element of {x,y} \ { the Element of {x,y}} by FUNCOP_1:def 8, GLIBPRE0:3;
A5: for x being object holds H₂([(the_Edges_of G),{x,x}]) = the Element of {x,x}

proof

let x be object ; :: thesis: H₂([(the_Edges_of G),{x,x}]) = the Element of {x,x}
A6: {x,x} \ { the Element of {x,x}} = {} by GLIBPRE0:3;
thus H₂([(the_Edges_of G),{x,x}]) = the Element of {x,x} by A6, FUNCOP_1:def 8; :: thesis: verum

end;

consider t being Function such that
A7: ( dom t = { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } & ( for x being object st x in { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } holds
t . x = H₂(x) ) ) from FUNCT_1:sch 3();

now :: thesis: for y being object st y in rng t holds
y in the_Vertices_of G

let y be object ; :: thesis: ( y in rng t implies b₁ in the_Vertices_of G )
assume y in rng t ; :: thesis: b₁ in the_Vertices_of G
then consider x being object such that
A8: ( x in dom t & t . x = y ) by FUNCT_1:def 3;
consider v, w being Vertex of G such that
A9: x = [(the_Edges_of G),{v,w}] and
for e being object holds not e Joins v,w,G by A7, A8;

per cases ( v <> w or v = w ) ;

suppose A10: v <> w ; :: thesis: b₁ in the_Vertices_of G

y = H₂([(the_Edges_of G),{v,w}]) by A7, A8, A9
.= the Element of {v,w} \ { the Element of {v,w}} by A4, A10 ;
then ( y = v or y = w ) by A10, GLIBPRE0:4;
hence y in the_Vertices_of G ; :: thesis: verum

end;

suppose A11: v = w ; :: thesis: b₁ in the_Vertices_of G

y = H₂([(the_Edges_of G),{v,w}]) by A7, A8, A9
.= the Element of {v,v} by A5, A11 ;
hence y in the_Vertices_of G ; :: thesis: verum

end;

end;

end;

then reconsider t = t as Function of { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,(the_Vertices_of G) by A7, TARSKI:def 3, FUNCT_2:2;
set H = createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t);

now :: thesis: for e1, e2, v1, v2 being object st e1 Joins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 Joins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) holds
e1 = e2

let e1, e2, v1, v2 be object ; :: thesis: ( e1 Joins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 Joins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) implies b₁ = b₂ )
assume A12: ( e1 Joins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 Joins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂
then e1 in the_Edges_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t)) by GLIB_000:def 13;
then A13: e1 in { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ;
then consider a, b being Vertex of G such that
A14: e1 = [(the_Edges_of G),{a,b}] and
for e being object holds not e Joins a,b,G ;
e2 in the_Edges_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t)) by A12, GLIB_000:def 13;
then A15: e2 in { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ;
then consider c, d being Vertex of G such that
A16: e2 = [(the_Edges_of G),{c,d}] and
for e being object holds not e Joins c,d,G ;

per cases ( ( a <> b & c <> d ) or ( a <> b & c = d ) or ( a = b & c <> d ) or ( a = b & c = d ) ) ;

suppose A17: ( a <> b & c <> d ) ; :: thesis: b₁ = b₂

per cases ( ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ) by A12, GLIB_000:16;

suppose A18: ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A19: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A18, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A20: v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A18, GLIB_000:def 14
.= t . e1
.= H<sub>2</sub>(e1) by A7, A13
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A17, A14 ;
A21: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A18, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A18, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A15
.= the Element of {c,d} \ { the Element of {c,d}} by A4, A17, A16 ;
then A22: ( ( v1 = c & v2 = d ) or ( v1 = d & v2 = c ) ) by A17, A21, GLIBPRE0:4;
( ( v1 = a & v2 = b ) or ( v1 = b & v2 = a ) ) by A17, A19, A20, GLIBPRE0:4;
hence e1 = e2 by A14, A16, A22; :: thesis: verum

end;

suppose A23: ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A24: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A23, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A25: v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A23, GLIB_000:def 14
.= t . e1
.= H<sub>2</sub>(e1) by A7, A13
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A17, A14 ;
A26: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A23, GLIB_000:def 14
.= t . e2
.= H<sub>2</sub>(e2) by A7, A15
.= the Element of {c,d} \ { the Element of {c,d}} by A4, A17, A16 ;
v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A23, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
then A27: ( ( v1 = c & v2 = d ) or ( v1 = d & v2 = c ) ) by A17, A26, GLIBPRE0:4;
( ( v1 = a & v2 = b ) or ( v1 = b & v2 = a ) ) by A17, A24, A25, GLIBPRE0:4;
hence e1 = e2 by A14, A16, A27; :: thesis: verum

end;

suppose A28: ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A29: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A28, GLIB_000:def 14
.= t . e1
.= H₂(e1) by A7, A13
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A17, A14 ;
A30: v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A28, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A31: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A28, GLIB_000:def 14
.= t . e2
.= H<sub>2</sub>(e2) by A7, A15
.= the Element of {c,d} \ { the Element of {c,d}} by A4, A17, A16 ;
v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A28, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
then A32: ( ( v1 = c & v2 = d ) or ( v1 = d & v2 = c ) ) by A17, A31, GLIBPRE0:4;
( ( v1 = a & v2 = b ) or ( v1 = b & v2 = a ) ) by A17, A29, A30, GLIBPRE0:4;
hence e1 = e2 by A14, A16, A32; :: thesis: verum

end;

suppose A33: ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A34: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A33, GLIB_000:def 14
.= t . e1
.= H₂(e1) by A7, A13
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A17, A14 ;
A35: v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A33, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A36: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A33, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A33, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A15
.= the Element of {c,d} \ { the Element of {c,d}} by A4, A17, A16 ;
then A37: ( ( v1 = c & v2 = d ) or ( v1 = d & v2 = c ) ) by A17, A36, GLIBPRE0:4;
( ( v1 = a & v2 = b ) or ( v1 = b & v2 = a ) ) by A17, A34, A35, GLIBPRE0:4;
hence e1 = e2 by A14, A16, A37; :: thesis: verum

end;

end;

end;

suppose A38: ( a <> b & c = d ) ; :: thesis: b₁ = b₂

per cases ( ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ) by A12, GLIB_000:16;

suppose A39: ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A40: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A39, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A41: v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A39, GLIB_000:def 14
.= t . e1
.= H<sub>2</sub>(e1) by A7, A13
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A38, A14 ;
A42: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A39, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
A43: v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A39, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A15
.= the Element of {c,d} by A5, A38, A16 ;
( ( v1 = a & v2 = b ) or ( v1 = b & v2 = a ) ) by A38, A40, A41, GLIBPRE0:4;
hence e1 = e2 by A38, A42, A43; :: thesis: verum

end;

suppose A44: ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A45: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A44, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A46: v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A44, GLIB_000:def 14
.= t . e1
.= H<sub>2</sub>(e1) by A7, A13
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A38, A14 ;
A47: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A44, GLIB_000:def 14
.= t . e2
.= H<sub>2</sub>(e2) by A7, A15
.= the Element of {c,d} by A5, A38, A16 ;
A48: v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A44, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
( ( v1 = a & v2 = b ) or ( v1 = b & v2 = a ) ) by A38, A45, A46, GLIBPRE0:4;
hence e1 = e2 by A38, A47, A48; :: thesis: verum

end;

suppose A49: ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A50: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A49, GLIB_000:def 14
.= t . e1
.= H₂(e1) by A7, A13
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A38, A14 ;
A51: v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A49, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A52: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A49, GLIB_000:def 14
.= t . e2
.= H<sub>2</sub>(e2) by A7, A15
.= the Element of {c,d} by A5, A38, A16 ;
A53: v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A49, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
( ( v1 = a & v2 = b ) or ( v1 = b & v2 = a ) ) by A38, A50, A51, GLIBPRE0:4;
hence e1 = e2 by A38, A52, A53; :: thesis: verum

end;

suppose A54: ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A55: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A54, GLIB_000:def 14
.= t . e1
.= H₂(e1) by A7, A13
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A38, A14 ;
A56: v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A54, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A57: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A54, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
A58: v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A54, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A15
.= the Element of {c,d} by A5, A38, A16 ;
( ( v1 = a & v2 = b ) or ( v1 = b & v2 = a ) ) by A38, A55, A56, GLIBPRE0:4;
hence e1 = e2 by A38, A57, A58; :: thesis: verum

end;

end;

end;

suppose A59: ( a = b & c <> d ) ; :: thesis: b₁ = b₂

per cases ( ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ) by A12, GLIB_000:16;

suppose A60: ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A61: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A60, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A62: v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A60, GLIB_000:def 14
.= t . e1
.= H<sub>2</sub>(e1) by A7, A13
.= the Element of {a,b} by A5, A59, A14 ;
A63: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A60, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A60, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A15
.= the Element of {c,d} \ { the Element of {c,d}} by A4, A59, A16 ;
then ( ( v1 = c & v2 = d ) or ( v1 = d & v2 = c ) ) by A59, A63, GLIBPRE0:4;
hence e1 = e2 by A59, A61, A62; :: thesis: verum

end;

suppose A64: ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A65: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A64, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A66: v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A64, GLIB_000:def 14
.= t . e1
.= H<sub>2</sub>(e1) by A7, A13
.= the Element of {a,b} by A5, A59, A14 ;
A67: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A64, GLIB_000:def 14
.= t . e2
.= H<sub>2</sub>(e2) by A7, A15
.= the Element of {c,d} \ { the Element of {c,d}} by A4, A59, A16 ;
v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A64, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
then ( ( v1 = c & v2 = d ) or ( v1 = d & v2 = c ) ) by A59, A67, GLIBPRE0:4;
hence e1 = e2 by A59, A65, A66; :: thesis: verum

end;

suppose A68: ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A69: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A68, GLIB_000:def 14
.= t . e1
.= H₂(e1) by A7, A13
.= the Element of {a,b} by A5, A59, A14 ;
A70: v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A68, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A71: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A68, GLIB_000:def 14
.= t . e2
.= H<sub>2</sub>(e2) by A7, A15
.= the Element of {c,d} \ { the Element of {c,d}} by A4, A59, A16 ;
v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A68, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
then ( ( v1 = c & v2 = d ) or ( v1 = d & v2 = c ) ) by A59, A71, GLIBPRE0:4;
hence e1 = e2 by A59, A69, A70; :: thesis: verum

end;

suppose A72: ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A73: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A72, GLIB_000:def 14
.= t . e1
.= H₂(e1) by A7, A13
.= the Element of {a,b} by A5, A59, A14 ;
A74: v2 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A72, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= the Element of {a,b} ;
A75: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A72, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= the Element of {c,d} ;
v2 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A72, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A15
.= the Element of {c,d} \ { the Element of {c,d}} by A4, A59, A16 ;
then ( ( v1 = c & v2 = d ) or ( v1 = d & v2 = c ) ) by A59, A75, GLIBPRE0:4;
hence e1 = e2 by A59, A73, A74; :: thesis: verum

end;

end;

end;

suppose A76: ( a = b & c = d ) ; :: thesis: b₁ = b₂

A77: ( {a,a} = {a} & {c,c} = {c} ) by ENUMSET1:29;

per cases ( ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) or ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ) by A12, GLIB_000:16;

suppose A78: ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A79: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A78, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= a by A76, A77, TARSKI:def 1 ;
v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A78, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= c by A76, A77, TARSKI:def 1 ;
hence e1 = e2 by A14, A16, A76, A79; :: thesis: verum

end;

suppose A80: ( e1 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A81: v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A80, GLIB_000:def 14
.= s . e1
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A13, A14
.= a by A76, A77, TARSKI:def 1 ;
v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A80, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A15
.= the Element of {c,d} by A5, A76, A16
.= c by A76, A77, TARSKI:def 1 ;
hence e1 = e2 by A14, A16, A76, A81; :: thesis: verum

end;

suppose A82: ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A83: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A82, GLIB_000:def 14
.= t . e1
.= H₂(e1) by A7, A13
.= the Element of {a,b} by A5, A76, A14
.= a by A76, A77, TARSKI:def 1 ;
v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A82, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A15
.= the Element of {c,d} by A5, A76, A16
.= c by A76, A77, TARSKI:def 1 ;
hence e1 = e2 by A14, A16, A76, A83; :: thesis: verum

end;

suppose A84: ( e1 DJoins v2,v1, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) & e2 DJoins v1,v2, createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) ) ; :: thesis: b₁ = b₂

A85: v1 = (the_Target_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e1 by A84, GLIB_000:def 14
.= t . e1
.= H₂(e1) by A7, A13
.= the Element of {a,b} by A5, A76, A14
.= a by A76, A77, TARSKI:def 1 ;
v1 = (the_Source_of (createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t))) . e2 by A84, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{c,d}] `2) by A1, A15, A16
.= c by A76, A77, TARSKI:def 1 ;
hence e1 = e2 by A14, A16, A76, A85; :: thesis: verum

end;

end;

end;

end;

end;

then reconsider H = createGraph ((the_Vertices_of G), { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ,s,t) as non-multi _Graph by GLIB_000:def 20;
take H ; :: thesis: ( the_Vertices_of H = the_Vertices_of G & the_Edges_of H misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,H ) ) )
thus the_Vertices_of H = the_Vertices_of G ; :: thesis: ( the_Edges_of H misses the_Edges_of G & ( for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,H ) ) )
{ [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } /\ (the_Edges_of G) = {}

proof

assume { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } /\ (the_Edges_of G) <> {} ; :: thesis: contradiction
then consider x being object such that
A86: x in { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } /\ (the_Edges_of G) by XBOOLE_0:def 1;
reconsider x = x as set by TARSKI:1;
x in { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } by A86, XBOOLE_0:def 4;
then consider v, w being Vertex of G such that
A87: x = [(the_Edges_of G),{v,w}] and
for e being object holds not e Joins v,w,G ;
A88: x in the_Edges_of G by A86, XBOOLE_0:def 4;
A89: the_Edges_of G in {(the_Edges_of G)} by TARSKI:def 1;
x = {{(the_Edges_of G),{v,w}},{(the_Edges_of G)}} by A87, TARSKI:def 5;
then {(the_Edges_of G)} in x by TARSKI:def 2;
hence contradiction by A88, A89, XREGULAR:7; :: thesis: verum

end;

then (the_Edges_of H) /\ (the_Edges_of G) = {} ;
hence the_Edges_of H misses the_Edges_of G by XBOOLE_0:def 7; :: thesis: for v, w being Vertex of G holds
( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,H )
let v, w be Vertex of G; :: thesis: ( ex e1 being object st e1 Joins v,w,G iff for e2 being object holds not e2 Joins v,w,H )

hereby :: thesis: ( ( for e2 being object holds not e2 Joins v,w,H ) implies ex e1 being object st e1 Joins v,w,G )

given e1 being object such that A90: e1 Joins v,w,G ; :: thesis: for e2 being object holds not e2 Joins v,w,H
given e2 being object such that A91: e2 Joins v,w,H ; :: thesis: contradiction
e2 in the_Edges_of H by A91, GLIB_000:def 13;
then A92: e2 in { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ;
then consider a, b being Vertex of G such that
A93: e2 = [(the_Edges_of G),{a,b}] and
A94: for e being object holds not e Joins a,b,G ;

per cases ( a <> b or a = b ) ;

suppose A95: a <> b ; :: thesis: contradiction

per cases ( e2 DJoins v,w,H or e2 DJoins w,v,H ) by A91, GLIB_000:16;

suppose A96: e2 DJoins v,w,H ; :: thesis: contradiction

A97: v = (the_Source_of H) . e2 by A96, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A92, A93
.= the Element of {a,b} ;
w = (the_Target_of H) . e2 by A96, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A92
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A93, A95 ;
then ( ( v = a & w = b ) or ( v = b & w = a ) ) by A95, A97, GLIBPRE0:4;
hence contradiction by A90, A94, GLIB_000:14; :: thesis: verum

end;

suppose A98: e2 DJoins w,v,H ; :: thesis: contradiction

A99: v = (the_Target_of H) . e2 by A98, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A92
.= the Element of {a,b} \ { the Element of {a,b}} by A4, A93, A95 ;
w = (the_Source_of H) . e2 by A98, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A92, A93
.= the Element of {a,b} ;
then ( ( v = a & w = b ) or ( v = b & w = a ) ) by A95, A99, GLIBPRE0:4;
hence contradiction by A90, A94, GLIB_000:14; :: thesis: verum

end;

end;

end;

suppose A100: a = b ; :: thesis: contradiction

A101: {a,a} = {a} by ENUMSET1:29;

per cases ( e2 DJoins v,w,H or e2 DJoins w,v,H ) by A91, GLIB_000:16;

suppose A102: e2 DJoins v,w,H ; :: thesis: contradiction

A103: v = (the_Source_of H) . e2 by A102, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A92, A93
.= a by A100, A101, TARSKI:def 1 ;
w = (the_Target_of H) . e2 by A102, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A92
.= the Element of {a,b} by A5, A93, A100
.= b by A100, A101, TARSKI:def 1 ;
hence contradiction by A90, A94, A103; :: thesis: verum

end;

suppose A104: e2 DJoins w,v,H ; :: thesis: contradiction

A105: v = (the_Target_of H) . e2 by A104, GLIB_000:def 14
.= t . e2
.= H₂(e2) by A7, A92
.= the Element of {a,b} by A5, A93, A100
.= a by A100, A101, TARSKI:def 1 ;
w = (the_Source_of H) . e2 by A104, GLIB_000:def 14
.= s . e2
.= the Element of Segm ([(the_Edges_of G),{a,b}] `2) by A1, A92, A93
.= b by A100, A101, TARSKI:def 1 ;
hence contradiction by A90, A94, A105; :: thesis: verum

end;

end;

end;

end;

end;

set e2 = [(the_Edges_of G),{v,w}];

now :: thesis: ( ( for e1 being object holds not e1 Joins v,w,G ) implies [(the_Edges_of G),{v,w}] Joins v,w,H )

assume for e1 being object holds not e1 Joins v,w,G ; :: thesis: [(the_Edges_of G),{v,w}] Joins v,w,H
then A106: [(the_Edges_of G),{v,w}] in { [(the_Edges_of G),{v,w}] where v, w is Vertex of G : for e being object holds not e Joins v,w,G } ;
then A107: [(the_Edges_of G),{v,w}] in the_Edges_of H ;

per cases ( v <> w or v = w ) ;

suppose A108: v <> w ; :: thesis: [(the_Edges_of G),{v,w}] Joins v,w,H

( the Element of {v,w} = the Element of {v,w} & the Element of {v,w} \ { the Element of {v,w}} = the Element of {v,w} \ { the Element of {v,w}} ) ;

per cases then ( ( v = the Element of {v,w} & w = the Element of {v,w} \ { the Element of {v,w}} ) or ( w = the Element of {v,w} & v = the Element of {v,w} \ { the Element of {v,w}} ) ) by A108, GLIBPRE0:4;

suppose A109: ( v = the Element of {v,w} & w = the Element of {v,w} \ { the Element of {v,w}} ) ; :: thesis: [(the_Edges_of G),{v,w}] Joins v,w,H

A110: v = the Element of Segm ([(the_Edges_of G),{v,w}] `2) by A109
.= s . [(the_Edges_of G),{v,w}] by A1, A106
.= (the_Source_of H) . [(the_Edges_of G),{v,w}] ;
w = H₂([(the_Edges_of G),{v,w}]) by A4, A108, A109
.= t . [(the_Edges_of G),{v,w}] by A7, A106
.= (the_Target_of H) . [(the_Edges_of G),{v,w}] ;
hence [(the_Edges_of G),{v,w}] Joins v,w,H by A107, A110, GLIB_000:def 13; :: thesis: verum

end;

suppose A111: ( w = the Element of {v,w} & v = the Element of {v,w} \ { the Element of {v,w}} ) ; :: thesis: [(the_Edges_of G),{v,w}] Joins v,w,H

A112: w = the Element of Segm ([(the_Edges_of G),{v,w}] `2) by A111
.= s . [(the_Edges_of G),{v,w}] by A1, A106
.= (the_Source_of H) . [(the_Edges_of G),{v,w}] ;
v = H₂([(the_Edges_of G),{v,w}]) by A4, A108, A111
.= t . [(the_Edges_of G),{v,w}] by A7, A106
.= (the_Target_of H) . [(the_Edges_of G),{v,w}] ;
hence [(the_Edges_of G),{v,w}] Joins v,w,H by A107, A112, GLIB_000:def 13; :: thesis: verum

end;

end;

end;

suppose A113: v = w ; :: thesis: [(the_Edges_of G),{v,w}] Joins v,w,H

A114: {v,v} = {v} by ENUMSET1:29;
A115: v = the Element of Segm ([(the_Edges_of G),{v,w}] `2) by A113, A114, TARSKI:def 1
.= s . [(the_Edges_of G),{v,w}] by A1, A106
.= (the_Source_of H) . [(the_Edges_of G),{v,w}] ;
w = the Element of Segm ([(the_Edges_of G),{v,w}] `2) by A113, A114, TARSKI:def 1
.= H₂([(the_Edges_of G),{v,w}]) by A5, A113
.= t . [(the_Edges_of G),{v,w}] by A7, A106
.= (the_Target_of H) . [(the_Edges_of G),{v,w}] ;
hence [(the_Edges_of G),{v,w}] Joins v,w,H by A107, A115, GLIB_000:def 13; :: thesis: verum

end;

end;

end;

hence ( ( for e2 being object holds not e2 Joins v,w,H ) implies ex e1 being object st e1 Joins v,w,G ) ; :: thesis: verum