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