let M be Pnet; :: thesis: ( (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} & (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} )
set S = id the Places of M;
thus (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} :: thesis: (f_enter M) * ((f_enter M) \ (id (Elements M))) = {}

proof

set R = the Flow of M | the Transitions of M;
A1: (id the Places of M) * (the Flow of M | the Transitions of M) = {} by Th17;
(f_exit M) * ((f_exit M) \ (id (Elements M))) = ((the Flow of M | the Transitions of M) \/ (id the Places of M)) * (the Flow of M | the Transitions of M) by Th19
.= ((the Flow of M | the Transitions of M) * (the Flow of M | the Transitions of M)) \/ ((id the Places of M) * (the Flow of M | the Transitions of M)) by SYSREL:20
.= {} by A1, Th16 ;
hence (f_exit M) * ((f_exit M) \ (id (Elements M))) = {} ; :: thesis: verum

end;

set R = (the Flow of M ~ ) | the Transitions of M;
A2: (id the Places of M) * ((the Flow of M ~ ) | the Transitions of M) = {} by Th17;
(f_enter M) * ((f_enter M) \ (id (Elements M))) = (((the Flow of M ~ ) | the Transitions of M) \/ (id the Places of M)) * ((the Flow of M ~ ) | the Transitions of M) by Th19
.= (((the Flow of M ~ ) | the Transitions of M) * ((the Flow of M ~ ) | the Transitions of M)) \/ ((id the Places of M) * ((the Flow of M ~ ) | the Transitions of M)) by SYSREL:20
.= {} by A2, Th16 ;
hence (f_enter M) * ((f_enter M) \ (id (Elements M))) = {} ; :: thesis: verum