for X being set
for g being SimpleGraph of X holds
( the carrier of g c= X & the SEdges of g c= TWOELEMENTSETS the carrier of g )