let N be Pnet; :: thesis: for x being Element of Elements N

for X being set st Elements N <> {} & x in X holds

exit (N,x) in Ext (N,X)

let x be Element of Elements N; :: thesis: for X being set st Elements N <> {} & x in X holds

exit (N,x) in Ext (N,X)

let X be set ; :: thesis: ( Elements N <> {} & x in X implies exit (N,x) in Ext (N,X) )

assume that

A1: Elements N <> {} and

A2: x in X ; :: thesis: exit (N,x) in Ext (N,X)

exit (N,x) c= Elements N by A1, Th19;

hence exit (N,x) in Ext (N,X) by A2, Def14; :: thesis: verum

for X being set st Elements N <> {} & x in X holds

exit (N,x) in Ext (N,X)

let x be Element of Elements N; :: thesis: for X being set st Elements N <> {} & x in X holds

exit (N,x) in Ext (N,X)

let X be set ; :: thesis: ( Elements N <> {} & x in X implies exit (N,x) in Ext (N,X) )

assume that

A1: Elements N <> {} and

A2: x in X ; :: thesis: exit (N,x) in Ext (N,X)

exit (N,x) c= Elements N by A1, Th19;

hence exit (N,x) in Ext (N,X) by A2, Def14; :: thesis: verum