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