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 object st [x,y] in f_pre M holds

[x,y] in [:(f_transitions M),(f_places M):]

[x,y] in [:(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

for x, y being object st [x,y] in f_post M holds
let x, y be object ; :: thesis: ( [x,y] in f_pre M implies [x,y] in [:(f_transitions M),(f_places M):] )

assume A2: [x,y] in f_pre M ; :: thesis: [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; :: thesis: verum

end;assume A2: [x,y] in f_pre M ; :: thesis: [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; :: thesis: verum

[x,y] in [:(f_transitions M),(f_places M):]

proof

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
let x, y be object ; :: thesis: ( [x,y] in f_post M implies [x,y] in [:(f_transitions M),(f_places M):] )

assume A4: [x,y] in f_post M ; :: thesis: [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; :: thesis: verum

end;assume A4: [x,y] in f_post M ; :: thesis: [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; :: thesis: verum