let X be set ; :: thesis: ( the carrier of (Tempty_f_net X) = X & the carrier' of (Tempty_f_net X) = {} & Flow (Tempty_f_net X) = {} )
Tempty_f_net X = PT_net_Str(# X,{},({} (X,{})),({} ({},X)) #) by Def1, XBOOLE_1:65;
hence ( the carrier of (Tempty_f_net X) = X & the carrier' of (Tempty_f_net X) = {} & Flow (Tempty_f_net X) = {} ) ; :: thesis: verum