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