let N be e_net; :: thesis: ( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N )
( the entrance of N c= [:the carrier of N,the carrier of N:] & the escape of N c= [:the carrier of N,the carrier of N:] ) by Def2;
hence ( dom the entrance of N c= the carrier of N & rng the entrance of N c= the carrier of N & dom the escape of N c= the carrier of N & rng the escape of N c= the carrier of N ) by SYSREL:15; :: thesis: verum