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