theorem :: SGRAPH1:20

for X being set
for g being SimpleGraph of X
for v1, v2 being set st {v1,v2} in the SEdges of g holds
( v1 in the carrier of g & v2 in the carrier of g & v1 <> v2 ) by Th10;