let N be Pnet; :: thesis: for x being Element of Elements N
for X being set st Elements N <> {} & x in X holds
enter N,x in Entr N,X
let x be Element of Elements N; :: thesis: for X being set st Elements N <> {} & x in X holds
enter N,x in Entr N,X
let X be set ; :: thesis: ( Elements N <> {} & x in X implies enter N,x in Entr N,X )
assume that
A1: Elements N <> {} and
A2: x in X ; :: thesis: enter N,x in Entr N,X
enter N,x c= Elements N by A1, Th23;
hence enter N,x in Entr N,X by A2, Def14; :: thesis: verum