per cases
( the_Edges_of G = {} or the_Edges_of G <> {} )
;

end;

suppose
the_Edges_of G = {}
; :: thesis: ex b_{1} being Subset of (the_Edges_of G) st

for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in b_{1} & ( for e9 being object st e9 DJoins v,w,G & e9 in b_{1} holds

e9 = e ) )

for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in b

e9 = e ) )

then A11:
G is edgeless
;

take {} (the_Edges_of G) ; :: thesis: for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in {} (the_Edges_of G) & ( for e9 being object st e9 DJoins v,w,G & e9 in {} (the_Edges_of G) holds

e9 = e ) )

thus for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in {} (the_Edges_of G) & ( for e9 being object st e9 DJoins v,w,G & e9 in {} (the_Edges_of G) holds

e9 = e ) ) by A11, GLIB_008:50; :: thesis: verum

end;take {} (the_Edges_of G) ; :: thesis: for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in {} (the_Edges_of G) & ( for e9 being object st e9 DJoins v,w,G & e9 in {} (the_Edges_of G) holds

e9 = e ) )

thus for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in {} (the_Edges_of G) & ( for e9 being object st e9 DJoins v,w,G & e9 in {} (the_Edges_of G) holds

e9 = e ) ) by A11, GLIB_008:50; :: thesis: verum

suppose A12:
the_Edges_of G <> {}
; :: thesis: ex b_{1} being Subset of (the_Edges_of G) st

for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in b_{1} & ( for e9 being object st e9 DJoins v,w,G & e9 in b_{1} holds

e9 = e ) )

for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in b

e9 = e ) )

set E = { the Element of Class ((DEdgeAdjEqRel G),e) where e is Element of the_Edges_of G : verum } ;

for x being object st x in { the Element of Class ((DEdgeAdjEqRel G),e) where e is Element of the_Edges_of G : verum } holds

x in the_Edges_of G

take E ; :: thesis: for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = e ) )

let v, w, e0 be object ; :: thesis: ( e0 DJoins v,w,G implies ex e being object st

( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = e ) ) )

assume A15: e0 DJoins v,w,G ; :: thesis: ex e being object st

( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = e ) )

then A16: e0 in the_Edges_of G by GLIB_000:def 14;

then reconsider e0 = e0 as Element of the_Edges_of G ;

set e = the Element of Class ((DEdgeAdjEqRel G),e0);

take the Element of Class ((DEdgeAdjEqRel G),e0) ; :: thesis: ( the Element of Class ((DEdgeAdjEqRel G),e0) DJoins v,w,G & the Element of Class ((DEdgeAdjEqRel G),e0) in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = the Element of Class ((DEdgeAdjEqRel G),e0) ) )

[e0,e0] in DEdgeAdjEqRel G by A15, EQREL_1:5, GLIB_000:def 14;

then Class ((DEdgeAdjEqRel G),e0) <> {} by RELAT_1:169;

then [e0, the Element of Class ((DEdgeAdjEqRel G),e0)] in DEdgeAdjEqRel G by EQREL_1:18;

then consider v1, v2 being object such that

A17: ( e0 DJoins v1,v2,G & the Element of Class ((DEdgeAdjEqRel G),e0) DJoins v1,v2,G ) by Def4;

( v = v1 & w = v2 ) by A15, A17, Th6;

hence the Element of Class ((DEdgeAdjEqRel G),e0) DJoins v,w,G by A17; :: thesis: ( the Element of Class ((DEdgeAdjEqRel G),e0) in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = the Element of Class ((DEdgeAdjEqRel G),e0) ) )

thus the Element of Class ((DEdgeAdjEqRel G),e0) in E ; :: thesis: for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = the Element of Class ((DEdgeAdjEqRel G),e0)

let e9 be object ; :: thesis: ( e9 DJoins v,w,G & e9 in E implies e9 = the Element of Class ((DEdgeAdjEqRel G),e0) )

assume A18: ( e9 DJoins v,w,G & e9 in E ) ; :: thesis: e9 = the Element of Class ((DEdgeAdjEqRel G),e0)

then consider e8 being Element of the_Edges_of G such that

A19: e9 = the Element of Class ((DEdgeAdjEqRel G),e8) ;

[e8,e8] in DEdgeAdjEqRel G by A16, EQREL_1:5;

then Class ((DEdgeAdjEqRel G),e8) <> {} by RELAT_1:169;

then A20: e9 in Class ((DEdgeAdjEqRel G),e8) by A19;

[e0,e9] in DEdgeAdjEqRel G by A15, A18, Def4;

then e9 in Class ((DEdgeAdjEqRel G),e0) by EQREL_1:18;

then Class ((DEdgeAdjEqRel G),e0) = Class ((DEdgeAdjEqRel G),e9) by EQREL_1:23

.= Class ((DEdgeAdjEqRel G),e8) by A20, EQREL_1:23 ;

hence e9 = the Element of Class ((DEdgeAdjEqRel G),e0) by A19; :: thesis: verum

end;for x being object st x in { the Element of Class ((DEdgeAdjEqRel G),e) where e is Element of the_Edges_of G : verum } holds

x in the_Edges_of G

proof

then reconsider E = { the Element of Class ((DEdgeAdjEqRel G),e) where e is Element of the_Edges_of G : verum } as Subset of (the_Edges_of G) by TARSKI:def 3;
let x be object ; :: thesis: ( x in { the Element of Class ((DEdgeAdjEqRel G),e) where e is Element of the_Edges_of G : verum } implies x in the_Edges_of G )

assume x in { the Element of Class ((DEdgeAdjEqRel G),e) where e is Element of the_Edges_of G : verum } ; :: thesis: x in the_Edges_of G

then consider e being Element of the_Edges_of G such that

A13: x = the Element of Class ((DEdgeAdjEqRel G),e) ;

[e,e] in DEdgeAdjEqRel G by A12, EQREL_1:5;

then Class ((DEdgeAdjEqRel G),e) <> {} by RELAT_1:169;

then [e,x] in DEdgeAdjEqRel G by A13, EQREL_1:18;

then consider v1, v2 being object such that

A14: ( e DJoins v1,v2,G & x DJoins v1,v2,G ) by Def4;

thus x in the_Edges_of G by A14, GLIB_000:def 14; :: thesis: verum

end;assume x in { the Element of Class ((DEdgeAdjEqRel G),e) where e is Element of the_Edges_of G : verum } ; :: thesis: x in the_Edges_of G

then consider e being Element of the_Edges_of G such that

A13: x = the Element of Class ((DEdgeAdjEqRel G),e) ;

[e,e] in DEdgeAdjEqRel G by A12, EQREL_1:5;

then Class ((DEdgeAdjEqRel G),e) <> {} by RELAT_1:169;

then [e,x] in DEdgeAdjEqRel G by A13, EQREL_1:18;

then consider v1, v2 being object such that

A14: ( e DJoins v1,v2,G & x DJoins v1,v2,G ) by Def4;

thus x in the_Edges_of G by A14, GLIB_000:def 14; :: thesis: verum

take E ; :: thesis: for v, w, e0 being object st e0 DJoins v,w,G holds

ex e being object st

( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = e ) )

let v, w, e0 be object ; :: thesis: ( e0 DJoins v,w,G implies ex e being object st

( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = e ) ) )

assume A15: e0 DJoins v,w,G ; :: thesis: ex e being object st

( e DJoins v,w,G & e in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = e ) )

then A16: e0 in the_Edges_of G by GLIB_000:def 14;

then reconsider e0 = e0 as Element of the_Edges_of G ;

set e = the Element of Class ((DEdgeAdjEqRel G),e0);

take the Element of Class ((DEdgeAdjEqRel G),e0) ; :: thesis: ( the Element of Class ((DEdgeAdjEqRel G),e0) DJoins v,w,G & the Element of Class ((DEdgeAdjEqRel G),e0) in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = the Element of Class ((DEdgeAdjEqRel G),e0) ) )

[e0,e0] in DEdgeAdjEqRel G by A15, EQREL_1:5, GLIB_000:def 14;

then Class ((DEdgeAdjEqRel G),e0) <> {} by RELAT_1:169;

then [e0, the Element of Class ((DEdgeAdjEqRel G),e0)] in DEdgeAdjEqRel G by EQREL_1:18;

then consider v1, v2 being object such that

A17: ( e0 DJoins v1,v2,G & the Element of Class ((DEdgeAdjEqRel G),e0) DJoins v1,v2,G ) by Def4;

( v = v1 & w = v2 ) by A15, A17, Th6;

hence the Element of Class ((DEdgeAdjEqRel G),e0) DJoins v,w,G by A17; :: thesis: ( the Element of Class ((DEdgeAdjEqRel G),e0) in E & ( for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = the Element of Class ((DEdgeAdjEqRel G),e0) ) )

thus the Element of Class ((DEdgeAdjEqRel G),e0) in E ; :: thesis: for e9 being object st e9 DJoins v,w,G & e9 in E holds

e9 = the Element of Class ((DEdgeAdjEqRel G),e0)

let e9 be object ; :: thesis: ( e9 DJoins v,w,G & e9 in E implies e9 = the Element of Class ((DEdgeAdjEqRel G),e0) )

assume A18: ( e9 DJoins v,w,G & e9 in E ) ; :: thesis: e9 = the Element of Class ((DEdgeAdjEqRel G),e0)

then consider e8 being Element of the_Edges_of G such that

A19: e9 = the Element of Class ((DEdgeAdjEqRel G),e8) ;

[e8,e8] in DEdgeAdjEqRel G by A16, EQREL_1:5;

then Class ((DEdgeAdjEqRel G),e8) <> {} by RELAT_1:169;

then A20: e9 in Class ((DEdgeAdjEqRel G),e8) by A19;

[e0,e9] in DEdgeAdjEqRel G by A15, A18, Def4;

then e9 in Class ((DEdgeAdjEqRel G),e0) by EQREL_1:18;

then Class ((DEdgeAdjEqRel G),e0) = Class ((DEdgeAdjEqRel G),e9) by EQREL_1:23

.= Class ((DEdgeAdjEqRel G),e8) by A20, EQREL_1:23 ;

hence e9 = the Element of Class ((DEdgeAdjEqRel G),e0) by A19; :: thesis: verum