let M be Pnet; :: thesis: ( f_pre M c= [:(f_transitions M),(f_places M):] & f_post M c= [:(f_transitions M),(f_places M):] )
A1:
for x, y being set st [x,y] in f_pre M holds
[x,y] in [:(f_transitions M),(f_places M):]
proof
let x,
y be
set ;
:: thesis: ( [x,y] in f_pre M implies [x,y] in [:(f_transitions M),(f_places M):] )
assume
[x,y] in f_pre M
;
:: thesis: [x,y] in [:(f_transitions M),(f_places M):]
then
(
x in the
Transitions of
M &
[x,y] in the
Flow of
M )
by RELAT_1:def 11;
then
(
x in f_transitions M &
y in the
Places of
M )
by Th11;
hence
[x,y] in [:(f_transitions M),(f_places M):]
by ZFMISC_1:106;
:: thesis: verum
end;
for x, y being set st [x,y] in f_post M holds
[x,y] in [:(f_transitions M),(f_places M):]
proof
let x,
y be
set ;
:: thesis: ( [x,y] in f_post M implies [x,y] in [:(f_transitions M),(f_places M):] )
assume
[x,y] in f_post M
;
:: thesis: [x,y] in [:(f_transitions M),(f_places M):]
then
(
x in the
Transitions of
M &
[x,y] in the
Flow of
M ~ )
by RELAT_1:def 11;
then
(
x in the
Transitions of
M &
[y,x] in the
Flow of
M )
by RELAT_1:def 7;
then
(
x in f_transitions M &
y in the
Places of
M )
by Th11;
hence
[x,y] in [:(f_transitions M),(f_places M):]
by ZFMISC_1:106;
:: thesis: verum
end;
hence
( f_pre M c= [:(f_transitions M),(f_places M):] & f_post M c= [:(f_transitions M),(f_places M):] )
by A1, RELAT_1:def 3; :: thesis: verum