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 DefSeqtLike;
seqt in S -sequents ;
then consider premises being Subset of (AllFormulasOf S), conclusion being wff string of S such that
B0: ( seqt = [premises,conclusion] & premises is finite ) ;
thus Sq `2 is wff string of S by B0, MCART_1:7; :: thesis: verum