let N be Pnet; :: thesis: for X being Subset of ()
for x being Element of Elements N st Elements N <> {} holds
( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) ) )

let X be Subset of (); :: thesis: for x being Element of Elements N st Elements N <> {} holds
( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) ) )

let x be Element of Elements N; :: thesis: ( Elements N <> {} implies ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) ) ) )

A1: ( ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) ) implies x in Input (N,X) )
proof
A2: ( ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) implies x in Input (N,X) )
proof
given y being Element of Elements N such that A3: y in X and
A4: y in the carrier' of N and
A5: pre N,y,x ; :: thesis: x in Input (N,X)
[x,y] in Flow N by A5;
then x in Pre (N,y) by ;
then A6: x in enter (N,y) by ;
enter (N,y) in Entr (N,X) by ;
hence x in Input (N,X) by ; :: thesis: verum
end;
A7: ( x in X & x in the carrier of N implies x in Input (N,X) )
proof
assume that
A8: x in X and
A9: x in the carrier of N ; :: thesis: x in Input (N,X)
( enter (N,x) = {x} & {x} c= Elements N ) by ;
then A10: {x} in Entr (N,X) by ;
x in {x} by TARSKI:def 1;
hence x in Input (N,X) by ; :: thesis: verum
end;
assume ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) ) ; :: thesis: x in Input (N,X)
hence x in Input (N,X) by A7, A2; :: thesis: verum
end;
assume A11: Elements N <> {} ; :: thesis: ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) ) )

( not x in Input (N,X) or ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) )
proof
assume x in Input (N,X) ; :: thesis: ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) )

then ex y being set st
( x in y & y in Entr (N,X) ) by TARSKI:def 4;
then consider y being set such that
A12: y in Entr (N,X) and
A13: x in y ;
consider z being Element of Elements N such that
A14: z in X and
A15: y = enter (N,z) by ;
A16: ( z in the carrier' of N implies y = Pre (N,z) ) by ;
A17: ( z in the carrier' of N implies ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) )
proof
assume A18: z in the carrier' of N ; :: thesis: ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x )

take z ; :: thesis: ( z in X & z in the carrier' of N & pre N,z,x )
[x,z] in Flow N by ;
hence ( z in X & z in the carrier' of N & pre N,z,x ) by ; :: thesis: verum
end;
A19: ( z in the carrier of N or z in the carrier' of N ) by ;
( z in the carrier of N implies y = {z} ) by ;
hence ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) ) by ; :: thesis: verum
end;
hence ( x in Input (N,X) iff ( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
( y in X & y in the carrier' of N & pre N,y,x ) ) ) by A1; :: thesis: verum