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 Joins v,w,G holds
ex e being object st
( e Joins v,w,G & e in b₁ & ( for e9 being object st e9 Joins v,w,G & e9 in b₁ holds
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;

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

proof

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;

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;
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

per cases ( ( v = v1 & w = v2 ) or ( v = v2 & w = v1 ) ) by A5, A7, GLIB_000:15;

suppose ( v = v1 & w = v2 ) ; :: thesis: the Element of Class ((EdgeAdjEqRel G),e0) Joins v,w,G

hence the Element of Class ((EdgeAdjEqRel G),e0) Joins v,w,G by A7; :: thesis: verum

end;

suppose ( v = v2 & w = v1 ) ; :: thesis: the Element of Class ((EdgeAdjEqRel G),e0) Joins v,w,G

hence the Element of Class ((EdgeAdjEqRel G),e0) Joins v,w,G by A7, GLIB_000:14; :: thesis: verum

end;

end;

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

end;

end;