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; verum