reconsider premises = x as finite Subset of ((AllSymbolsOf S) *) by XBOOLE_1:2;
premises c= AllFormulasOf S by XBOOLE_1:2;
then [premises,phi] in S -sequents ;
hence [x,phi] is Element of S -sequents ; :: thesis: verum