let M be Pnet; :: thesis: ( f_prox M c= [:(Elements M),(Elements M):] & f_flow M c= [:(Elements M),(Elements M):] )
A1: the Flow of M | the Places of M c= the Flow of M by RELAT_1:88;
the Flow of M c= [:(Elements M),(Elements M):] by Th13;
then A2: the Flow of M | the Places of M c= [:(Elements M),(Elements M):] by A1, XBOOLE_1:1;
A3: (the Flow of M ~ ) | the Places of M c= the Flow of M ~ by RELAT_1:88;
the Flow of M ~ c= [:(Elements M),(Elements M):] by Th13;
then A4: (the Flow of M ~ ) | the Places of M c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:1;
the Places of M c= Elements M by XBOOLE_1:7;
then A5: [:the Places of M,the Places of M:] c= [:(Elements M),(Elements M):] by ZFMISC_1:119;
id the Places of M c= [:the Places of M,the Places of M:] by RELSET_1:28;
then A6: id the Places of M c= [:(Elements M),(Elements M):] by A5, XBOOLE_1:1;
(the Flow of M | the Places of M) \/ ((the Flow of M ~ ) | the Places of M) c= [:(Elements M),(Elements M):] by A2, A4, XBOOLE_1:8;
hence f_prox M c= [:(Elements M),(Elements M):] by A6, XBOOLE_1:8; :: thesis: f_flow M c= [:(Elements M),(Elements M):]
A7: the Flow of M c= [:(Elements M),(Elements M):] by Th13;
id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:28;
hence f_flow M c= [:(Elements M),(Elements M):] by A7, XBOOLE_1:8; :: thesis: verum