theorem :: GLIB_000:11

for GS being GraphStruct
for x being set holds
( the_Vertices_of (GS .set (VertexSelector,x)) = x & the_Edges_of (GS .set (EdgeSelector,x)) = x & the_Source_of (GS .set (SourceSelector,x)) = x & the_Target_of (GS .set (TargetSelector,x)) = x ) by Th8;