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