let N be Pnet; :: thesis: for X being Subset of (Elements N)

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 (Elements N); :: 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) )

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

( y in X & y in the carrier' of N & pre N,y,x ) ) ) by A1; :: thesis: verum

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 (Elements N); :: 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

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

( 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;( y in X & y in the carrier' of N & pre N,y,x ) implies x in Input (N,X) )

proof

A7:
( x in X & x in the carrier of N implies x in Input (N,X) )
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 A4, Def6;

then A6: x in enter (N,y) by A4, Def8;

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

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

end;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 A4, Def6;

then A6: x in enter (N,y) by A4, Def8;

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

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

proof

assume
( ( x in X & x in the carrier of N ) or ex y being Element of Elements N st
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 A9, Def8, ZFMISC_1:31;

then A10: {x} in Entr (N,X) by A8, Def13;

x in {x} by TARSKI:def 1;

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

end;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 A9, Def8, ZFMISC_1:31;

then A10: {x} in Entr (N,X) by A8, Def13;

x in {x} by TARSKI:def 1;

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

( 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

( 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

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
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 A12, Def13;

A16: ( z in the carrier' of N implies y = Pre (N,z) ) by A15, Def8;

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

( z in the carrier of N implies y = {z} ) by A15, Def8;

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 A13, A14, A19, A17, TARSKI:def 1; :: thesis: verum

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

A16: ( z in the carrier' of N implies y = Pre (N,z) ) by A15, Def8;

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

A19:
( z in the carrier of N or z in the carrier' of N )
by A11, XBOOLE_0:def 3;
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 A13, A16, A18, Def6;

hence ( z in X & z in the carrier' of N & pre N,z,x ) by A14, A18; :: thesis: verum

end;( 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 A13, A16, A18, Def6;

hence ( z in X & z in the carrier' of N & pre N,z,x ) by A14, A18; :: thesis: verum

( z in the carrier of N implies y = {z} ) by A15, Def8;

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 A13, A14, A19, A17, TARSKI:def 1; :: thesis: verum

( y in X & y in the carrier' of N & pre N,y,x ) ) ) by A1; :: thesis: verum