let M be Pnet; :: thesis: ( (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} & (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} )
set R = the Flow of M | the Places of M;
set S = id the Transitions of M;
thus (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} :: thesis: (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {}

proof

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

end;

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