defpred S₁[ object , object ] means ex v1, v2 being object st
( $1 DJoins v1,v2,G & $2 DJoins v1,v2,G );
A12: 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 A13: e in the_Edges_of G ; :: thesis: S₁[e,e]
take (the_Source_of G) . e ; :: thesis: ex v2 being object st
( e DJoins (the_Source_of G) . e,v2,G & e DJoins (the_Source_of G) . e,v2,G )
take (the_Target_of G) . e ; :: thesis: ( e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G & e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G )
thus ( e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G & e DJoins (the_Source_of G) . e,(the_Target_of G) . e,G ) by A13, GLIB_000:def 14; :: thesis: verum

end;

A14: for e1, e2 being object st S₁[e1,e2] holds
S₁[e2,e1] ;
A15: 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 A16: ( S₁[e1,e2] & S₁[e2,e3] ) ; :: thesis: S₁[e1,e3]
then consider v1, v2 being object such that
A17: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ;
consider v3, v4 being object such that
A18: ( e2 DJoins v3,v4,G & e3 DJoins v3,v4,G ) by A16;
take v1 ; :: thesis: ex v2 being object st
( e1 DJoins v1,v2,G & e3 DJoins v1,v2,G )
take v2 ; :: thesis: ( e1 DJoins v1,v2,G & e3 DJoins v1,v2,G )
( v1 = v3 & v2 = v4 ) by A17, A18, GLIB_000:125;
hence ( e1 DJoins v1,v2,G & e3 DJoins v1,v2,G ) by A17, A18; :: thesis: verum

end;

consider EqR being Equivalence_Relation of (the_Edges_of G) such that
A19: 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(A12, A14, A15);
take EqR ; :: thesis: for e1, e2 being object holds
( [e1,e2] in EqR iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) )
let e1, e2 be object ; :: thesis: ( [e1,e2] in EqR iff ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) )
thus ( [e1,e2] in EqR implies ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ) by A19; :: thesis: ( ex v1, v2 being object st
( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) implies [e1,e2] in EqR )
given v1, v2 being object such that A20: ( e1 DJoins v1,v2,G & e2 DJoins v1,v2,G ) ; :: thesis: [e1,e2] in EqR
( e1 in the_Edges_of G & e2 in the_Edges_of G ) by A20, GLIB_000:def 14;
hence [e1,e2] in EqR by A19, A20; :: thesis: verum