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

.= 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