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 Output 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 & post N,y,x ) ) )
let X be Subset of (Elements N); :: thesis: for x being Element of Elements N st Elements N <> {} holds
( x in Output 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 & post N,y,x ) ) )
let x be Element of Elements N; :: thesis: ( Elements N <> {} implies ( x in Output 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 & post 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 & post N,y,x ) ) implies x in Output N,X )

proof

A2: ( ex y being Element of Elements N st
( y in X & y in the carrier' of N & post N,y,x ) implies x in Output 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: post N,y,x ; :: thesis: x in Output N,X
[y,x] in Flow N by A5, Def6;
then x in Post N,y by A4, Def8;
then A6: x in exit N,y by A4, Def10;
exit N,y in Ext N,X by A3, Th29;
hence x in Output N,X by A6, TARSKI:def 4; :: thesis: verum

end;

A7: ( x in X & x in the carrier of N implies x in Output N,X )

proof

assume that
A8: x in X and
A9: x in the carrier of N ; :: thesis: x in Output N,X
( exit N,x = {x} & {x} c= Elements N ) by A9, Def10, ZFMISC_1:37;
then A10: {x} in Ext N,X by A8, Def15;
x in {x} by TARSKI:def 1;
hence x in Output N,X by A10, TARSKI:def 4; :: 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 & post N,y,x ) ) ; :: thesis: x in Output N,X
hence x in Output N,X by A7, A2; :: thesis: verum

end;

assume A11: Elements N <> {} ; :: thesis: ( x in Output 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 & post N,y,x ) ) )
( not x in Output 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 & post N,y,x ) )

proof

assume x in Output 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 & post N,y,x ) )
then ex y being set st
( x in y & y in Ext N,X ) by TARSKI:def 4;
then consider y being set such that
A12: y in Ext N,X and
A13: x in y ;
consider z being Element of Elements N such that
A14: z in X and
A15: y = exit N,z by A12, Def15;
A16: ( z in the carrier' of N implies y = Post N,z ) by A15, Def10;
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 & post 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 & post N,y,x )
take z ; :: thesis: ( z in X & z in the carrier' of N & post N,z,x )
[z,x] in Flow N by A13, A16, A18, Def8;
hence ( z in X & z in the carrier' of N & post N,z,x ) by A14, A18, Def6; :: thesis: verum

end;

A19: ( z in the carrier of N or z in the carrier' of N ) by A11, XBOOLE_0:def 3;
( z in the carrier of N implies y = {z} ) by A15, Def10;
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 & post N,y,x ) ) by A13, A14, A19, A17, TARSKI:def 1; :: thesis: verum

end;

hence ( x in Output 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 & post N,y,x ) ) ) by A1; :: thesis: verum