let M be Pnet; :: thesis: ( f_exit M c= [:(Elements M),(Elements M):] & f_enter M c= [:(Elements M),(Elements M):] )
A1: id the Places of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:28;
then A2: id the Places of M c= [:(Elements M),(Elements M):] by A1, XBOOLE_1:1;
A3: the Flow of M | the Transitions of M c= the Flow of M by RELAT_1:88;
the Flow of M c= [:(Elements M),(Elements M):] by Th13;
then the Flow of M | the Transitions 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 Places of M c= id (Elements M) by SYSREL:33, XBOOLE_1:7;
id (Elements M) c= [:(Elements M),(Elements M):] by RELSET_1:28;
then A5: id the Places of M c= [:(Elements M),(Elements M):] by A4, XBOOLE_1:1;
A6: (the Flow of M ~ ) | the Transitions of M c= the Flow of M ~ by RELAT_1:88;
the Flow of M ~ c= [:(Elements M),(Elements M):] by Th13;
then (the Flow of M ~ ) | the Transitions 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