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;