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