:: deftheorem Def68 defines Correct FOMODEL4:def 68 :
for S being Language
for R being Rule of S holds
( R is Correct iff for X being set st X is S -correct holds
R . X is S -correct );