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