let X be set ; :: thesis: for S being Language
for phi being wff string of S st phi in X holds
phi is X,{(R#0 S)} -provable
let S be Language; :: thesis: for phi being wff string of S st phi in X holds
phi is X,{(R#0 S)} -provable
let phi be wff string of S; :: thesis: ( phi in X implies phi is X,{(R#0 S)} -provable )
assume phi in X ; :: thesis: phi is X,{(R#0 S)} -provable
then reconsider Xphi = {phi} as Subset of X by ZFMISC_1:31;
{[{phi},phi]} is {} ,{(R#0 S)} -derivable ;
then phi is Xphi,{(R#0 S)} -provable ;
hence phi is X,{(R#0 S)} -provable ; :: thesis: verum