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 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)) = {} ) ; :: thesis: verum