theorem :: E_SIEC:1

for X being set
for R, S being Relation holds
( G_Net(# X,R,S #) is e_net iff ( R c= [:X,X:] & S c= [:X,X:] & R * R = R & R * S = R & S * S = S & S * R = S & R * (R \ (id X)) = {} & S * (S \ (id X)) = {} ) ) by Def1, Def2;