:: deftheorem defines Extract ALGSTR_1:def 1 :
for x being set holds Extract x = x;