set FF = AllFormulasOf S;
set Q = S -sequents ;
Sq in S -sequents by Def2;
then consider premises being Subset of (AllFormulasOf S), conclusion being wff string of S such that
A1: ( Sq = [premises,conclusion] & premises is finite ) ;
thus for b₁ being set st b₁ = Sq `1 holds
b₁ is S -premises-like by A1; :: thesis: verum