let N be Pnet; 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 ; ( 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) ) )
assume A4:
X c= Elements N
; ( 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) )
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; verum