theorem Th9: :: SCMYCIEL:9

for X being set
for s being Subset of X st s is 1 -element holds
ex x being set st
( x in X & s = {x} )