:: deftheorem defines Bool_marks_of BOOLMARK:def 1 :
for PTN being PT_net_Str holds Bool_marks_of PTN = Funcs ( the carrier of PTN,BOOLEAN);