theorem :: PRE_POLY:7

for A being set holds {} |_2 A = {} ;