:: deftheorem Def2 defines EE E_SIEC:def 2 :
for IT being G_Net holds
( IT is EE iff ( the entrance of IT * ( the entrance of IT \ (id the carrier of IT)) = {} & the escape of IT * ( the escape of IT \ (id the carrier of IT)) = {} ) );