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 = (Flow M) | the carrier of M;
set S = id the carrier' of M;
A1: (id the carrier' of M) * ((Flow M) | the carrier of M) = {} by Th12;
(f_escape M) * ((f_escape M) \ (id (Elements M))) = (((Flow M) | the carrier of M) \/ (id the carrier' of M)) * ((Flow M) | the carrier of M) by Th14
.= (((Flow M) | the carrier of M) * ((Flow M) | the carrier of M)) \/ ((id the carrier' of M) * ((Flow M) | the carrier of M)) by SYSREL:6
.= {} by A1, Th11 ;
hence (f_escape M) * ((f_escape M) \ (id (Elements M))) = {} ; :: thesis: (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {}
set R = ((Flow M) ~) | the carrier of M;
A2: (id the carrier' of M) * (((Flow M) ~) | the carrier of M) = {} by Th12;
(f_entrance M) * ((f_entrance M) \ (id (Elements M))) = ((((Flow M) ~) | the carrier of M) \/ (id the carrier' of M)) * (((Flow M) ~) | the carrier of M) by Th14
.= ((((Flow M) ~) | the carrier of M) * (((Flow M) ~) | the carrier of M)) \/ ((id the carrier' of M) * (((Flow M) ~) | the carrier of M)) by SYSREL:6
.= {} by A2, Th11 ;
hence (f_entrance M) * ((f_entrance M) \ (id (Elements M))) = {} ; :: thesis: verum