let N be Pnet; 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); 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; ( 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
;
x in Output (N,X)
[y,x] in Flow N
by A5;
then
x in Post (
N,
y)
by A4, Def7;
then A6:
x in exit (
N,
y)
by A4, Def9;
exit (
N,
y)
in Ext (
N,
X)
by A3, Th22;
hence
x in Output (
N,
X)
by A6, TARSKI:def 4;
verum
end;
A7:
(
x in X &
x in the
carrier of
N implies
x in Output (
N,
X) )
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 ) )
;
x in Output (N,X)
hence
x in Output (
N,
X)
by A7, A2;
verum
end;
assume A11:
Elements N <> {}
; ( 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)
;
( ( 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, Def14;
A16:
(
z in the
carrier' of
N implies
y = Post (
N,
z) )
by A15, Def9;
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
;
ex y being Element of Elements N st
( y in X & y in the carrier' of N & post N,y,x )
take
z
;
( z in X & z in the carrier' of N & post N,z,x )
[z,x] in Flow N
by A13, A16, A18, Def7;
hence
(
z in X &
z in the
carrier' of
N &
post N,
z,
x )
by A14, A18;
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, Def9;
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;
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; verum