:: deftheorem defines SinglRel FIN_TOPO:def 2 :
for x being set holds SinglRel x = {[x,x]};