set Q = S -sequents ;
set IT = {} /\ S;
reconsider ITT = {} /\ S as Subset of (S -sequents) by XBOOLE_1:2;
ITT is S -sequents-like ;
hence for b₁ being set st b₁ = {} /\ S holds
b₁ is S -sequents-like ; :: thesis: verum