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

( 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