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