theorem :: NET_1:1

for x being set
for N being PT_net_Str holds
( not Elements N <> {} or not x is Element of Elements N or x is Element of the carrier of N or x is Element of the carrier' of N ) by XBOOLE_0:def 3;