let N be Pnet; :: thesis: for x being Element of Elements N st Elements N <> {} holds
enter N,x c= Elements N
let x be Element of Elements N; :: thesis: ( Elements N <> {} implies enter N,x c= Elements N )
assume A1: Elements N <> {} ; :: thesis: enter N,x c= Elements N
A2: ( enter N,x = {x} implies enter N,x c= Elements N )

proof

x in Elements N by A1;
then A3: for y being set st y in {x} holds
y in Elements N by TARSKI:def 1;
assume enter N,x = {x} ; :: thesis: enter N,x c= Elements N
hence enter N,x c= Elements N by A3, TARSKI:def 3; :: thesis: verum

end;

( enter N,x = {x} or enter N,x = Pre N,x ) by A1, Th22;
hence enter N,x c= Elements N by A2, Th16; :: thesis: verum