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, Th16;

hence enter (N,x) in Entr (N,X) by A2, Def13; :: thesis: verum

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, Th16;

hence enter (N,x) in Entr (N,X) by A2, Def13; :: thesis: verum