set AF = AllFormulasOf S;
set premises = the finite Subset of (AllFormulasOf S);
set conclusion = the wff string of S;
[ the finite Subset of (AllFormulasOf S), the wff string of S] in S -sequents ;
hence not S -sequents is empty ; :: thesis: verum