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