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