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) ) )

( 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) )

( y in X & x in exit (N,y) ) ) by A1; :: thesis: verum

( 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 A4:
X c= Elements N
; :: thesis: ( x in Output (N,X) iff ex y being Element of Elements N st
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;( 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

( 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

hence
( x in Output (N,X) iff ex y being Element of Elements N st
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;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

( y in X & x in exit (N,y) ) ) by A1; :: thesis: verum