let N be Pnet; 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 Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x ) ) )
let X be 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 Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x ) ) )
let x be Element of Elements N; ( Elements N <> {} implies ( x in Input N,X iff ( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x ) ) ) )
A1:
( ( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions 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
Transitions 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
Transitions of
N
and A5:
pre N,
y,
x
;
x in Input N,X
[x,y] in the
Flow of
N
by A5, Def5;
then
x in Pre N,
y
by A4, Def7;
then A6:
x in enter N,
y
by A4, Def9;
enter N,
y in Entr N,
X
by A3, Th28;
hence
x in Input N,
X
by A6, TARSKI:def 4;
verum
end;
A7:
(
x in X &
x in the
Places of
N implies
x in Input N,
X )
assume
( (
x in X &
x in the
Places of
N ) or ex
y being
Element of
Elements N st
(
y in X &
y in the
Transitions of
N &
pre N,
y,
x ) )
;
x in Input N,X
hence
x in Input N,
X
by A7, A2;
verum
end;
assume A11:
Elements N <> {}
; ( x in Input N,X iff ( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x ) ) )
( not x in Input N,X or ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x ) )
proof
assume
x in Input N,
X
;
( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions 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, Def14;
A16:
(
z in the
Transitions of
N implies
y = Pre N,
z )
by A15, Def9;
A17:
(
z in the
Transitions of
N implies ex
y being
Element of
Elements N st
(
y in X &
y in the
Transitions of
N &
pre N,
y,
x ) )
proof
assume A18:
z in the
Transitions of
N
;
ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x )
take
z
;
( z in X & z in the Transitions of N & pre N,z,x )
[x,z] in the
Flow of
N
by A13, A16, A18, Def7;
hence
(
z in X &
z in the
Transitions of
N &
pre N,
z,
x )
by A14, A18, Def5;
verum
end;
A19:
(
z in the
Places of
N or
z in the
Transitions of
N )
by A11, XBOOLE_0:def 3;
(
z in the
Places of
N implies
y = {z} )
by A15, Def9;
hence
( (
x in X &
x in the
Places of
N ) or ex
y being
Element of
Elements N st
(
y in X &
y in the
Transitions of
N &
pre N,
y,
x ) )
by A13, A14, A19, A17, TARSKI:def 1;
verum
end;
hence
( x in Input N,X iff ( ( x in X & x in the Places of N ) or ex y being Element of Elements N st
( y in X & y in the Transitions of N & pre N,y,x ) ) )
by A1; verum