:: deftheorem SingleFunc defines singleton ROUGHS_5:def 2 :
for R being non empty set
for b₂ being Function of R,(bool R) holds
( b₂ = singleton R iff for x being Element of R holds b₂ . x = {x} );