let S be Language; :: thesis: for Sq being S -sequent-like object holds Sq `2 is wff string of S
let Sq be S -sequent-like object ; :: 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; :: thesis: verum