let G1, G2 be _Graph; ( G1 tolerates G2 iff for e, v1, w1, v2, w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds
( v1 = v2 & w1 = w2 ) )
hereby ( ( for e, v1, w1, v2, w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds
( v1 = v2 & w1 = w2 ) ) implies G1 tolerates G2 )
assume A1:
G1 tolerates G2
;
for e, v1, w1, v2, w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds
( v1 = v2 & w1 = w2 )let e,
v1,
w1,
v2,
w2 be
object ;
( e DJoins v1,w1,G1 & e DJoins v2,w2,G2 implies ( v1 = v2 & w1 = w2 ) )assume A2:
(
e DJoins v1,
w1,
G1 &
e DJoins v2,
w2,
G2 )
;
( v1 = v2 & w1 = w2 )then A3:
(
e in the_Edges_of G1 &
e in the_Edges_of G2 )
by GLIB_000:def 14;
then
(
e in dom (the_Source_of G1) &
e in dom (the_Source_of G2) )
by FUNCT_2:def 1;
then A4:
e in (dom (the_Source_of G1)) /\ (dom (the_Source_of G2))
by XBOOLE_0:def 4;
thus v1 =
(the_Source_of G1) . e
by A2, GLIB_000:def 14
.=
(the_Source_of G2) . e
by A1, A4, PARTFUN1:def 4
.=
v2
by A2, GLIB_000:def 14
;
w1 = w2
(
e in dom (the_Target_of G1) &
e in dom (the_Target_of G2) )
by A3, FUNCT_2:def 1;
then A5:
e in (dom (the_Target_of G1)) /\ (dom (the_Target_of G2))
by XBOOLE_0:def 4;
thus w1 =
(the_Target_of G1) . e
by A2, GLIB_000:def 14
.=
(the_Target_of G2) . e
by A1, A5, PARTFUN1:def 4
.=
w2
by A2, GLIB_000:def 14
;
verum
end;
assume A6:
for e, v1, w1, v2, w2 being object st e DJoins v1,w1,G1 & e DJoins v2,w2,G2 holds
( v1 = v2 & w1 = w2 )
; G1 tolerates G2
hence
the_Source_of G1 tolerates the_Source_of G2
by PARTFUN1:def 4; GLIB_014:def 22 the_Target_of G1 tolerates the_Target_of G2
hence
the_Target_of G1 tolerates the_Target_of G2
by PARTFUN1:def 4; verum