set AF = AllFormulasOf S;
reconsider Phi = {} as finite Subset of (AllFormulasOf S) by XBOOLE_1:2;
[(Phi \/ {phi}),phi] is 1, {} ,{(R#0 S)} -derivable ;
hence for b₁ being object st b₁ = [{phi},phi] holds
b₁ is 1, {} ,{(R#0 S)} -derivable ; :: thesis: verum