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 )
A1: dom the entrance of N c= the carrier of N

proof

the entrance of N c= [:the carrier of N,the carrier of N:] by Def2;
hence dom the entrance of N c= the carrier of N by SYSREL:15; :: thesis: verum

end;

A2: rng the entrance of N c= the carrier of N

proof

the entrance of N c= [:the carrier of N,the carrier of N:] by Def2;
hence rng the entrance of N c= the carrier of N by SYSREL:15; :: thesis: verum

end;

A3: dom the escape of N c= the carrier of N

proof

the escape of N c= [:the carrier of N,the carrier of N:] by Def2;
hence dom the escape of N c= the carrier of N by SYSREL:15; :: thesis: verum

end;

rng the escape of N c= the carrier of N

proof

the escape of N c= [:the carrier of N,the carrier of N:] by Def2;
hence rng the escape of N c= the carrier of N by SYSREL:15; :: thesis: verum

end;

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 A1, A2, A3; :: thesis: verum