:: deftheorem Def8 defines enter NET_1:def 8 :
for N being Pnet
for x being Element of Elements N st Elements N <> {} holds
for b₃ being set holds
( b₃ = enter (N,x) iff ( ( x in the carrier of N implies b₃ = {x} ) & ( x in the carrier' of N implies b₃ = Pre (N,x) ) ) );