theorem :: RPR_1:7

for E being non empty set ex e being Singleton of E st e is Singleton of E