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