thus dom ((F | (dom F)) _V) = dom ((F _V) | (dom (F _V))) by Th54
.= the_Vertices_of (dom F) by Th54 ; :: according to GLIB_010:def 11 :: thesis: dom ((F | (dom F)) _E) = the_Edges_of (dom F)
thus dom ((F | (dom F)) _E) = dom ((F _E) | (dom (F _E))) by Th54
.= the_Edges_of (dom F) by Th54 ; :: thesis: verum