let S be GraphUnionSet; :: thesis: for G being GraphUnion of S
for e, v, w being object st e DJoins v,w,G holds
ex H being Element of S st e DJoins v,w,H
let G be GraphUnion of S; :: thesis: for e, v, w being object st e DJoins v,w,G holds
ex H being Element of S st e DJoins v,w,H
let e, v, w be object ; :: thesis: ( e DJoins v,w,G implies ex H being Element of S st e DJoins v,w,H )
assume e DJoins v,w,G ; :: thesis: ex H being Element of S st e DJoins v,w,H
then A1: ( e in the_Edges_of G & (the_Source_of G) . e = v & (the_Target_of G) . e = w ) by GLIB_000:def 14;
e in union (the_Edges_of S) by A1, GLIB_014:def 25;
then consider E being set such that
A2: ( e in E & E in the_Edges_of S ) by TARSKI:def 4;
consider H being _Graph such that
A3: ( H in S & E = the_Edges_of H ) by A2, GLIB_014:def 15;
reconsider H = H as Element of S by A3;
take H ; :: thesis: e DJoins v,w,H
A4: ( e in dom (the_Source_of H) & e in dom (the_Target_of H) ) by A2, A3, FUNCT_2:def 1;
the_Source_of H in the_Source_of S by GLIB_014:def 16;
then A5: (the_Source_of H) . e = (union (the_Source_of S)) . e by A4, COMPUT_1:13
.= v by A1, GLIB_014:def 25 ;
the_Target_of H in the_Target_of S by GLIB_014:def 17;
then (the_Target_of H) . e = (union (the_Target_of S)) . e by A4, COMPUT_1:13
.= w by A1, GLIB_014:def 25 ;
hence e DJoins v,w,H by A2, A3, A5, GLIB_000:def 14; :: thesis: verum