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, Def15; :: thesis: verum