set FF = AllFormulasOf S;
reconsider XX = X as finite Subset of (AllFormulasOf S) by Def4;
let Y be Subset of X; :: thesis: Y is S -premises-like
Y is Subset of XX ;
hence Y is S -premises-like by XBOOLE_1:1; :: thesis: verum