theorem :: E_SIEC:9

for x being object holds
( the carrier of (Tsingle_e_net x) = {x} & the entrance of (Tsingle_e_net x) = {} & the escape of (Tsingle_e_net x) = {} ) ;