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, Def14;
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, Th22;
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