theorem :: NET_1:3

for x being set
for N being PT_net_Str st x is Element of the carrier' of N & the carrier' of N <> {} holds
x is Element of Elements N by XBOOLE_1:7, TARSKI:def 3;