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 Joins v,w,G holds

ex e being object st

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

e9 = e ) )

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

ex e being object st

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

e9 = e ) )

then A1:
G is edgeless
;

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

ex e being object st

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

e9 = e ) )

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

ex e being object st

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

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

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

ex e being object st

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

e9 = e ) )

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

ex e being object st

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

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

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

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

ex e being object st

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

e9 = e ) )

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

ex e being object st

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

e9 = e ) )

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

for x being object st x in { the Element of Class ((EdgeAdjEqRel 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 Joins v,w,G holds

ex e being object st

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

e9 = e ) )

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

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

e9 = e ) ) )

assume A5: e0 Joins v,w,G ; :: thesis: ex e being object st

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

e9 = e ) )

then A6: e0 in the_Edges_of G by GLIB_000:def 13;

then reconsider e0 = e0 as Element of the_Edges_of G ;

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

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

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

[e0,e0] in EdgeAdjEqRel G by A6, EQREL_1:5;

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

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

then consider v1, v2 being object such that

A7: ( e0 Joins v1,v2,G & the Element of Class ((EdgeAdjEqRel G),e0) Joins v1,v2,G ) by Def3;

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

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

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

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

assume A8: ( e9 Joins v,w,G & e9 in E ) ; :: thesis: e9 = the Element of Class ((EdgeAdjEqRel G),e0)

then consider e8 being Element of the_Edges_of G such that

A9: e9 = the Element of Class ((EdgeAdjEqRel G),e8) ;

[e8,e8] in EdgeAdjEqRel G by A6, EQREL_1:5;

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

then A10: e9 in Class ((EdgeAdjEqRel G),e8) by A9;

[e0,e9] in EdgeAdjEqRel G by A5, A8, Def3;

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

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

.= Class ((EdgeAdjEqRel G),e8) by A10, EQREL_1:23 ;

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

end;for x being object st x in { the Element of Class ((EdgeAdjEqRel 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 ((EdgeAdjEqRel 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 ((EdgeAdjEqRel 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 ((EdgeAdjEqRel 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

A3: x = the Element of Class ((EdgeAdjEqRel G),e) ;

[e,e] in EdgeAdjEqRel G by A2, EQREL_1:5;

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

then [e,x] in EdgeAdjEqRel G by A3, EQREL_1:18;

then consider v1, v2 being object such that

A4: ( e Joins v1,v2,G & x Joins v1,v2,G ) by Def3;

thus x in the_Edges_of G by A4, GLIB_000:def 13; :: thesis: verum

end;assume x in { the Element of Class ((EdgeAdjEqRel 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

A3: x = the Element of Class ((EdgeAdjEqRel G),e) ;

[e,e] in EdgeAdjEqRel G by A2, EQREL_1:5;

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

then [e,x] in EdgeAdjEqRel G by A3, EQREL_1:18;

then consider v1, v2 being object such that

A4: ( e Joins v1,v2,G & x Joins v1,v2,G ) by Def3;

thus x in the_Edges_of G by A4, GLIB_000:def 13; :: thesis: verum

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

ex e being object st

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

e9 = e ) )

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

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

e9 = e ) ) )

assume A5: e0 Joins v,w,G ; :: thesis: ex e being object st

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

e9 = e ) )

then A6: e0 in the_Edges_of G by GLIB_000:def 13;

then reconsider e0 = e0 as Element of the_Edges_of G ;

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

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

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

[e0,e0] in EdgeAdjEqRel G by A6, EQREL_1:5;

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

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

then consider v1, v2 being object such that

A7: ( e0 Joins v1,v2,G & the Element of Class ((EdgeAdjEqRel G),e0) Joins v1,v2,G ) by Def3;

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

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

proof
end;

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

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

assume A8: ( e9 Joins v,w,G & e9 in E ) ; :: thesis: e9 = the Element of Class ((EdgeAdjEqRel G),e0)

then consider e8 being Element of the_Edges_of G such that

A9: e9 = the Element of Class ((EdgeAdjEqRel G),e8) ;

[e8,e8] in EdgeAdjEqRel G by A6, EQREL_1:5;

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

then A10: e9 in Class ((EdgeAdjEqRel G),e8) by A9;

[e0,e9] in EdgeAdjEqRel G by A5, A8, Def3;

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

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

.= Class ((EdgeAdjEqRel G),e8) by A10, EQREL_1:23 ;

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