defpred S1[ 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
S1[e,e]
proof
let e be
object ;
( e in the_Edges_of G implies S1[e,e] )
assume A13:
e in the_Edges_of G
;
S1[e,e]
take
(the_Source_of G) . e
;
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
;
( 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;
verum
end;
A14:
for e1, e2 being object st S1[e1,e2] holds
S1[e2,e1]
;
A15:
for e1, e2, e3 being object st S1[e1,e2] & S1[e2,e3] holds
S1[e1,e3]
proof
let e1,
e2,
e3 be
object ;
( S1[e1,e2] & S1[e2,e3] implies S1[e1,e3] )
assume A16:
(
S1[
e1,
e2] &
S1[
e2,
e3] )
;
S1[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
;
ex v2 being object st
( e1 DJoins v1,v2,G & e3 DJoins v1,v2,G )
take
v2
;
( e1 DJoins v1,v2,G & e3 DJoins v1,v2,G )
(
v1 = v3 &
v2 = v4 )
by A17, A18, Th6;
hence
(
e1 DJoins v1,
v2,
G &
e3 DJoins v1,
v2,
G )
by A17, A18;
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 & S1[e1,e2] ) )
from EQREL_1:sch 1(A12, A14, A15);
take
EqR
; 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 ; ( [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; ( 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 )
; [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; verum