theorem :: E_SIEC:8

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