let M be Pnet; :: thesis: ( f_prox M c= [:(Elements M),(Elements M):] & f_flow M c= [:(Elements M),(Elements M):] )
A1: (Flow M) | the carrier of M c= Flow M by RELAT_1:88;
Flow M c= [:(Elements M),(Elements M):] by Th13;
then A2: (Flow M) | the carrier of M c= [:(Elements M),(Elements M):] by A1, XBOOLE_1:1;
A3: ((Flow M) ~ ) | the carrier of M c= (Flow M) ~ by RELAT_1:88;
(Flow M) ~ c= [:(Elements M),(Elements M):] by Th13;
then A4: ((Flow M) ~ ) | the carrier of M c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:1;
the carrier of M c= Elements M by XBOOLE_1:7;
then A5: [:the carrier of M,the carrier of M:] c= [:(Elements M),(Elements M):] by ZFMISC_1:119;
id the carrier of M c= [:the carrier of M,the carrier of M:] by RELSET_1:28;
then A6: id the carrier of M c= [:(Elements M),(Elements M):] by A5, XBOOLE_1:1;
((Flow M) | the carrier of M) \/ (((Flow M) ~ ) | the carrier 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: Flow 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