reconsider f = F _V , g = F _E as one-to-one Function ;
let e, v, w be object ; :: according to GLIB_010:def 17 :: thesis: ( e in dom ((F ") _E) & v in dom ((F ") _V) & w in dom ((F ") _V) & ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 implies e DJoins v,w,G2 )
assume ( e in dom ((F ") _E) & v in dom ((F ") _V) & w in dom ((F ") _V) ) ; :: thesis: ( not ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 or e DJoins v,w,G2 )
then A1: ( e in rng g & v in rng f & w in rng f ) by FUNCT_1:33;
then consider e0 being object such that
A2: ( e0 in dom g & g . e0 = e ) by FUNCT_1:def 3;
consider v0 being object such that
A3: ( v0 in dom f & f . v0 = v ) by A1, FUNCT_1:def 3;
consider w0 being object such that
A4: ( w0 in dom f & f . w0 = w ) by A1, FUNCT_1:def 3;
assume ((F ") _E) . e DJoins ((F ") _V) . v,((F ") _V) . w,G1 ; :: thesis: e DJoins v,w,G2
then (g ") . (g . e0) DJoins (f ") . (f . v0),w0,G1 by A2, A3, A4, FUNCT_1:34;
then (g ") . (g . e0) DJoins v0,w0,G1 by A3, FUNCT_1:34;
then e0 DJoins v0,w0,G1 by A2, FUNCT_1:34;
hence e DJoins v,w,G2 by A2, A3, A4, Th16; :: thesis: verum