set FF = AllFormulasOf S;
set Q = S -sequents ;
Sq in S -sequents by DefSeqtLike;
then consider premises being Subset of (AllFormulasOf S), conclusion being wff string of S such that
B0: ( Sq = [premises,conclusion] & premises is finite ) ;
Sq `1 = premises by B0, MCART_1:7;
hence for b<sub>1</sub> being set st b<sub>1</sub> = Sq `1 holds
b₁ is S -premises-like by B0, DefPremLike; :: thesis: verum