theorem Th25: :: SCMYCIEL:25

for x being set holds {{},{x}} is SimpleGraph