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