:: deftheorem defines Psingle_f_net FF_SIEC:def 5 :
for x being object holds Psingle_f_net x = PTempty_f_net ({x},{});