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 )

hence enter (N,x) c= Elements N by A2, Th9; :: thesis: verum

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

( enter (N,x) = {x} or enter (N,x) = Pre (N,x) )
by A1, Th15;
x in Elements N
by A1;

then A3: for y being object 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;then A3: for y being object 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

hence enter (N,x) c= Elements N by A2, Th9; :: thesis: verum