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

proof

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

end;

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

proof

given y being Element of Elements N such that A5: y in X and
A6: x in enter N,y ; :: thesis: x in Input N,X
enter N,y in Entr N,X by A4, A5, Th28;
hence x in Input N,X by A6, TARSKI:def 4; :: thesis: verum

end;

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