let S be Language; :: thesis: for Sq being S -sequent-like set holds Sq `2 is wff string of S
let Sq be S -sequent-like set ; :: thesis: Sq `2 is wff string of S
set Q = S -sequents ;
reconsider seqt = Sq as Element of S -sequents by Def2;
seqt in S -sequents ;
then consider premises being Subset of (AllFormulasOf S), conclusion being wff string of S such that
A1: ( seqt = [premises,conclusion] & premises is finite ) ;
thus Sq `2 is wff string of S by A1, MCART_1:7; :: thesis: verum