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