set SS = AllSymbolsOf S;
set strings = ((AllSymbolsOf S) *) \ {{}};
set FF = AllFormulasOf S;
now :: thesis: for z being object st z in S -sequents holds
z in [:(bool (AllFormulasOf S)),(((AllSymbolsOf S) *) \ {{}}):]
let z be object ; :: thesis: ( z in S -sequents implies z in [:(bool (AllFormulasOf S)),(((AllSymbolsOf S) *) \ {{}}):] )
assume z in S -sequents ; :: thesis: z in [:(bool (AllFormulasOf S)),(((AllSymbolsOf S) *) \ {{}}):]
then consider x being Subset of (AllFormulasOf S), y being wff string of S such that
A1: ( z = [x,y] & x is finite ) ;
thus z in [:(bool (AllFormulasOf S)),(((AllSymbolsOf S) *) \ {{}}):] by A1; :: thesis: verum
end;
then S -sequents is Subset of [:(bool (AllFormulasOf S)),(((AllSymbolsOf S) *) \ {{}}):] by TARSKI:def 3;
hence S -sequents is Relation-like ; :: thesis: verum