theorem Th24: :: E_SIEC:24

for N being e_net holds
( ( the escape of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the escape of N \ (id the carrier of N)) * ( the entrance of N \ (id the carrier of N)) = {} & ( the entrance of N \ (id the carrier of N)) * ( the escape of N \ (id the carrier of N)) = {} )