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

suppose the_Edges_of G = {} ; :: thesis: ex b₁ 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₁ & ( for e9 being object st e9 DJoins v,w,G & e9 in b₁ holds
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;

suppose A12: the_Edges_of G <> {} ; :: thesis: ex b₁ 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₁ & ( for e9 being object st e9 DJoins v,w,G & e9 in b₁ holds
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

proof

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;

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;
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, GLIB_000:125;
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;

end;