:: deftheorem defines empty_f_net FF_SIEC:def 6 :
empty_f_net = PTempty_f_net ({},{});