empty_f_net = PT_net_Str(# {} ,{} ,({} {} ,{} ),({} {} ,{} ) #) by Def4, XBOOLE_1:65;
hence ( the carrier of empty_f_net = {} & the carrier' of empty_f_net = {} & Flow empty_f_net = {} ) ; :: thesis: verum