let M be Pnet; :: thesis: ( () * (() \ (id ())) = {} & () * (() \ (id ())) = {} )
set S = id the carrier of M;
thus (f_exit M) * (() \ (id ())) = {} :: thesis: () * (() \ (id ())) = {}
proof
set R = (Flow M) | the carrier' of M;
A1: (id the carrier of M) * ((Flow M) | the carrier' of M) = {} by Th12;
() * (() \ (id ())) = (((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 ;
hence (f_exit M) * (() \ (id ())) = {} ; :: thesis: verum
end;
set R = ((Flow M) ~) | the carrier' of M;
A2: (id the carrier of M) * (((Flow M) ~) | the carrier' of M) = {} by Th12;
() * (() \ (id ())) = ((((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 ;
hence (f_enter M) * (() \ (id ())) = {} ; :: thesis: verum