:: deftheorem defines MPS PARSP_1:def 11 :
for F being Field holds MPS F = ParStr(# (C_3 F),(PR F) #);