let M be Pnet; ( 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 object st [x,y] in f_pre M holds
[x,y] in [:(f_transitions M),(f_places M):]
proof
let x,
y be
object ;
( [x,y] in f_pre M implies [x,y] in [:(f_transitions M),(f_places M):] )
assume A2:
[x,y] in f_pre M
;
[x,y] in [:(f_transitions M),(f_places M):]
then A3:
x in the
carrier' of
M
by RELAT_1:def 11;
[x,y] in Flow M
by A2, RELAT_1:def 11;
then
y in the
carrier of
M
by A3, Th7;
hence
[x,y] in [:(f_transitions M),(f_places M):]
by A3, ZFMISC_1:87;
verum
end;
for x, y being object st [x,y] in f_post M holds
[x,y] in [:(f_transitions M),(f_places M):]
proof
let x,
y be
object ;
( [x,y] in f_post M implies [x,y] in [:(f_transitions M),(f_places M):] )
assume A4:
[x,y] in f_post M
;
[x,y] in [:(f_transitions M),(f_places M):]
then A5:
[x,y] in (Flow M) ~
by RELAT_1:def 11;
A6:
x in the
carrier' of
M
by A4, RELAT_1:def 11;
[y,x] in Flow M
by A5, RELAT_1:def 7;
then
y in the
carrier of
M
by A6, Th7;
hence
[x,y] in [:(f_transitions M),(f_places M):]
by A6, ZFMISC_1:87;
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; verum