let X, Y be set ; :: thesis: G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net
A1: id (X \ Y) c= [:X,X:]

proof

X \ Y c= X by XBOOLE_1:36;
then A2: [:(X \ Y),(X \ Y):] c= [:X,X:] by ZFMISC_1:119;
id (X \ Y) c= [:(X \ Y),(X \ Y):] by RELSET_1:28;
hence id (X \ Y) c= [:X,X:] by A2, XBOOLE_1:1; :: thesis: verum

end;

A3: (id (X \ Y)) * (id (X \ Y)) = id (X \ Y) by SYSREL:29;
(id (X \ Y)) * ((id (X \ Y)) \ (id X)) = (id (X \ Y)) * {} by SYSREL:34
.= {} ;
hence G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net by A1, A3, Def2, Def3; :: thesis: verum