let X, Y be set ; ( 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
; ( 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 Def1;
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)) = {} )
; verum