:: deftheorem defines s_pre E_SIEC:def 20 :
for N being G_Net holds s_pre N = ( the escape of N \ (id the carrier of N)) ~ ;