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, Th26;
hence exit N,x in Ext N,X by A2, Def15; :: thesis: verum