let M be Pnet; :: thesis: ( f_exit M c= [:(Elements M),(Elements M):] & f_enter M c= [:(Elements M),(Elements M):] )
A1: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:13;
then A2: id 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:59;
Flow M c= [:(Elements M),(Elements M):] by Th8;
then (Flow M) | the carrier' of M c= [:(Elements M),(Elements M):] by A3, XBOOLE_1:1;
hence f_exit M c= [:(Elements M),(Elements M):] by A2, XBOOLE_1:8; :: thesis: f_enter M c= [:(Elements M),(Elements M):]
A4: id the carrier of M c= id (Elements M) by SYSREL:15, XBOOLE_1:7;
id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:13;
then A5: id the carrier of M c= [:(Elements M),(Elements M):] by A4, XBOOLE_1:1;
A6: ((Flow M) ~) | the carrier' of M c= (Flow M) ~ by RELAT_1:59;
(Flow M) ~ c= [:(Elements M),(Elements M):] by Th8;
then ((Flow M) ~) | the carrier' of M c= [:(Elements M),(Elements M):] by A6, XBOOLE_1:1;
hence f_enter M c= [:(Elements M),(Elements M):] by A5, XBOOLE_1:8; :: thesis: verum