:: deftheorem defines return SCMPDS_2:def 5 :
for a being Int_position holds return a = [1,{},<*a*>];