set M = Net(# X,Y,{} #);
( the Places of Net(# X,Y,{} #) misses the Transitions of 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 A1, XBOOLE_1:2;
hence Net(# X,Y,{} #) is strict Pnet by NET_1:def 1; :: thesis: verum