let X, Y be set ; :: thesis: G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net
A1: (id (X \ Y)) * ((id (X \ Y)) \ (id X)) = (id (X \ Y)) * {} by SYSREL:16
.= {} ;
X \ Y c= X by XBOOLE_1:36;
then A2: [:(X \ Y),(X \ Y):] c= [:X,X:] by ZFMISC_1:96;
id (X \ Y) c= [:(X \ Y),(X \ Y):] by RELSET_1:13;
then A3: id (X \ Y) c= [:X,X:] by A2, XBOOLE_1:1;
(id (X \ Y)) * (id (X \ Y)) = id (X \ Y) by SYSREL:12;
hence G_Net(# X,(id (X \ Y)),(id (X \ Y)) #) is e_net by A3, A1, Def1, Def2; :: thesis: verum