for X being set
for S being Language
for phi being wff string of S st phi in X holds
phi is X,{(R#0 S)} -provable