:: deftheorem defines [#] WEIERSTR:def 1 :
for P being Subset of R^1 holds [#] P = P;