theorem :: RPR_1:12
for E being non empty set
for e1, e2 being Singleton of E holds
( e1 = e2 or e1 misses e2 )