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