set M = Net(# X,Y,{} #);
the Flow of Net(# X,Y,{} #) c= [:the Places of Net(# X,Y,{} #),the Transitions of Net(# X,Y,{} #):] \/ [:the Transitions of Net(# X,Y,{} #),the Places of Net(# X,Y,{} #):] by XBOOLE_1:2;
hence Net(# X,Y,{} #) is strict Pnet by A1, NET_1:def 1; :: thesis: verum