let N be Pnet; :: thesis: for x, X being set st X c= Elements N holds
( x in Output N,X iff ex y being Element of Elements N st
( y in X & x in exit N,y ) )
let x, X be set ; :: thesis: ( X c= Elements N implies ( x in Output N,X iff ex y being Element of Elements N st
( y in X & x in exit N,y ) ) )
A1: ( x in Output N,X implies ex y being Element of Elements N st
( y in X & x in exit N,y ) )

proof

assume x in Output N,X ; :: thesis: ex y being Element of Elements N st
( y in X & x in exit N,y )
then consider y being set such that
A2: x in y and
A3: y in Ext N,X by TARSKI:def 4;
ex z being Element of Elements N st
( z in X & y = exit N,z ) by A3, Def15;
hence ex y being Element of Elements N st
( y in X & x in exit N,y ) by A2; :: thesis: verum

end;

assume A4: X c= Elements N ; :: thesis: ( x in Output N,X iff ex y being Element of Elements N st
( y in X & x in exit N,y ) )
( ex y being Element of Elements N st
( y in X & x in exit N,y ) implies x in Output N,X )

proof

given y being Element of Elements N such that A5: y in X and
A6: x in exit N,y ; :: thesis: x in Output N,X
exit N,y in Ext N,X by A4, A5, Th29;
hence x in Output N,X by A6, TARSKI:def 4; :: thesis: verum

end;

hence ( x in Output N,X iff ex y being Element of Elements N st
( y in X & x in exit N,y ) ) by A1; :: thesis: verum