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

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

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

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

hence ex y being Element of Elements N st

( y in X & x in enter (N,y) ) by A2; :: thesis: verum

end;( 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, Def13;

hence ex y being Element of Elements N st

( y in X & x in enter (N,y) ) by A2; :: thesis: verum

( 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

hence
( x in Input (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 enter (N,y) ; :: thesis: x in Input (N,X)

enter (N,y) in Entr (N,X) by A4, A5, Th21;

hence x in Input (N,X) by A6, TARSKI:def 4; :: thesis: verum

end;A6: x in enter (N,y) ; :: thesis: x in Input (N,X)

enter (N,y) in Entr (N,X) by A4, A5, Th21;

hence x in Input (N,X) by A6, TARSKI:def 4; :: thesis: verum

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