:: deftheorem defines R#3d FOMODEL4:def 53 :
for S being Language holds R#3d S = FuncRule (P#3d S);