defpred S₁[ object , object ] means ex v1, v2 being object st
( $1 Joins v1,v2,G & $2 Joins v1,v2,G );
A1: for e being object st e in the_Edges_of G holds
S₁[e,e]

proof

let e be object ; :: thesis: ( e in the_Edges_of G implies S₁[e,e] )
assume A2: e in the_Edges_of G ; :: thesis: S₁[e,e]
take (the_Source_of G) . e ; :: thesis: ex v2 being object st
( e Joins (the_Source_of G) . e,v2,G & e Joins (the_Source_of G) . e,v2,G )
take (the_Target_of G) . e ; :: thesis: ( e Joins (the_Source_of G) . e,(the_Target_of G) . e,G & e Joins (the_Source_of G) . e,(the_Target_of G) . e,G )
thus ( e Joins (the_Source_of G) . e,(the_Target_of G) . e,G & e Joins (the_Source_of G) . e,(the_Target_of G) . e,G ) by A2, GLIB_000:def 13; :: thesis: verum

end;

A3: for e1, e2 being object st S₁[e1,e2] holds
S₁[e2,e1] ;
A4: for e1, e2, e3 being object st S₁[e1,e2] & S₁[e2,e3] holds
S₁[e1,e3]

proof

let e1, e2, e3 be object ; :: thesis: ( S₁[e1,e2] & S₁[e2,e3] implies S₁[e1,e3] )
assume A5: ( S₁[e1,e2] & S₁[e2,e3] ) ; :: thesis: S₁[e1,e3]
then consider v1, v2 being object such that
A6: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ;
consider v3, v4 being object such that
A7: ( e2 Joins v3,v4,G & e3 Joins v3,v4,G ) by A5;
take v1 ; :: thesis: ex v2 being object st
( e1 Joins v1,v2,G & e3 Joins v1,v2,G )
take v2 ; :: thesis: ( e1 Joins v1,v2,G & e3 Joins v1,v2,G )
thus e1 Joins v1,v2,G by A6; :: thesis: e3 Joins v1,v2,G

per cases ( ( v1 = v3 & v2 = v4 ) or ( v1 = v4 & v2 = v3 ) ) by A6, A7, GLIB_000:15;

suppose ( v1 = v3 & v2 = v4 ) ; :: thesis: e3 Joins v1,v2,G

hence e3 Joins v1,v2,G by A7; :: thesis: verum

end;

suppose ( v1 = v4 & v2 = v3 ) ; :: thesis: e3 Joins v1,v2,G

hence e3 Joins v1,v2,G by A7, GLIB_000:14; :: thesis: verum

end;

end;

end;

consider EqR being Equivalence_Relation of (the_Edges_of G) such that
A8: for e1, e2 being object holds
( [e1,e2] in EqR iff ( e1 in the_Edges_of G & e2 in the_Edges_of G & S₁[e1,e2] ) ) from EQREL_1:sch 1(A1, A3, A4);
take EqR ; :: thesis: for e1, e2 being object holds
( [e1,e2] in EqR iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) )
let e1, e2 be object ; :: thesis: ( [e1,e2] in EqR iff ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) )
thus ( [e1,e2] in EqR implies ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ) by A8; :: thesis: ( ex v1, v2 being object st
( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) implies [e1,e2] in EqR )
given v1, v2 being object such that A9: ( e1 Joins v1,v2,G & e2 Joins v1,v2,G ) ; :: thesis: [e1,e2] in EqR
( e1 in the_Edges_of G & e2 in the_Edges_of G ) by A9, GLIB_000:def 13;
hence [e1,e2] in EqR by A8, A9; :: thesis: verum