:: deftheorem defines Elements NET_1:def 3 :
for N being PT_net_Str holds Elements N = the carrier of N \/ the carrier' of N;