theorem Th31: :: SCMYCIEL:31

for X being set ex G being SimpleGraph st
( G is edgeless & Vertices G = X )