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 ;
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 ; :: 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