:: deftheorem defines Example MIDSP_1:def 2 :
Example = MidStr(# {0},op2 #);