:: deftheorem defines PR PARSP_1:def 10 :
for F being Field holds PR F = PRs F;