set x = [premises,phi];
set Q = S -sequents ;
[premises,phi] in S -sequents ;
hence for b₁ being set st b₁ = [premises,phi] holds
b₁ is S -sequent-like ; :: thesis: verum