set N = PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #);
thus the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) /\ the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) = {} ; :: according to XBOOLE_0:def 7,NET_1:def 2 :: thesis: Flow PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) c= [: the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] \/ [: the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):]
thus Flow PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #) c= [: the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] \/ [: the carrier' of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #), the carrier of PT_net_Str(# {},{},({} ({},{})),({} ({},{})) #):] ; :: thesis: verum