:: deftheorem defines Pempty_f_net FF_SIEC:def 3 :
for X being set holds Pempty_f_net X = PTempty_f_net ({},X);