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, Def15;
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