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 Def1;
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:3; :: thesis: verum