let N be Pnet; for x being Element of Elements N st Elements N <> {} holds
enter (N,x) c= Elements N
let x be Element of Elements N; ( Elements N <> {} implies enter (N,x) c= Elements N )
assume A1:
Elements N <> {}
; enter (N,x) c= Elements N
A2:
( enter (N,x) = {x} implies enter (N,x) c= Elements N )
( enter (N,x) = {x} or enter (N,x) = Pre (N,x) )
by A1, Th15;
hence
enter (N,x) c= Elements N
by A2, Th9; verum