:: deftheorem defines -provable FOMODEL4:def 69 :
for X being set
for S being Language
for phi being wff string of S holds
( phi is X -provable iff phi is X,{(R#9 S)} \/ (S -rules) -provable );