let x be object ; :: thesis: ( the carrier of (Tsingle_f_net x) = {} & the carrier' of (Tsingle_f_net x) = {x} & Flow (Tsingle_f_net x) = {} )
{} misses {x} by XBOOLE_1:65;
then Tsingle_f_net x = PT_net_Str(# {},{x},({} ({},{x})),({} ({x},{})) #) by Def1;
hence ( the carrier of (Tsingle_f_net x) = {} & the carrier' of (Tsingle_f_net x) = {x} & Flow (Tsingle_f_net x) = {} ) ; :: thesis: verum