theorem :: FUNCT_3:41

for Y being set
for A being Subset of Y holds incl A = (id Y) | A by Th1;