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