:: deftheorem Def1 defines PTempty_f_net FF_SIEC:def 1 :
for X, Y being set st X misses Y holds
PTempty_f_net (X,Y) = PT_net_Str(# X,Y,({} (X,Y)),({} (Y,X)) #);