theorem Th1: :: RPR_1:1

for E being non empty set
for e being non empty Subset of E holds
( e is Singleton of E iff for Y being set holds
( Y c= e iff ( Y = {} or Y = e ) ) )