:: deftheorem defines f_places FF_SIEC:def 11 :
for M being Pnet holds f_places M = the carrier of M;