:: deftheorem defines <* FINSEQ_1:def 5 :
for x being object holds <*x*> = {[1,x]};