let X, Y be set ; :: thesis: ( X misses Y implies ( the carrier of (PTempty_f_net X,Y) = X & the carrier' of (PTempty_f_net X,Y) = Y & Flow (PTempty_f_net X,Y) = {} ) )
assume X misses Y ; :: thesis: ( the carrier of (PTempty_f_net X,Y) = X & the carrier' of (PTempty_f_net X,Y) = Y & Flow (PTempty_f_net X,Y) = {} )
then PTempty_f_net X,Y = PT_net_Str(# X,Y,({} X,Y),({} Y,X) #) by Def4;
hence ( the carrier of (PTempty_f_net X,Y) = X & the carrier' of (PTempty_f_net X,Y) = Y & Flow (PTempty_f_net X,Y) = {} ) ; :: thesis: verum