thus ( id G is total & not id G is empty & id G is onto & id G is one-to-one ) ; :: thesis: id G is Dcontinuous
let e9, v, w be object ; :: according to GLIB_010:def 18 :: thesis: ( v in dom ((id G) _V) & w in dom ((id G) _V) & e9 DJoins ((id G) _V) . v,((id G) _V) . w,G implies ex e being object st
( e DJoins v,w,G & e in dom ((id G) _E) & ((id G) _E) . e = e9 ) )
assume that
A1: ( v in dom ((id G) _V) & w in dom ((id G) _V) ) and
A2: e9 DJoins ((id G) _V) . v,((id G) _V) . w,G ; :: thesis: ex e being object st
( e DJoins v,w,G & e in dom ((id G) _E) & ((id G) _E) . e = e9 )
take e9 ; :: thesis: ( e9 DJoins v,w,G & e9 in dom ((id G) _E) & ((id G) _E) . e9 = e9 )
e9 DJoins ((id G) _V) . v,w,G by A1, A2, FUNCT_1:18;
hence e9 DJoins v,w,G by A1, FUNCT_1:18; :: thesis: ( e9 in dom ((id G) _E) & ((id G) _E) . e9 = e9 )
A3: e9 in the_Edges_of G by A2, GLIB_000:def 14;
hence e9 in dom ((id G) _E) ; :: thesis: ((id G) _E) . e9 = e9
thus ((id G) _E) . e9 = e9 by A3, FUNCT_1:18; :: thesis: verum