consider t being set such that
A1: t in Terminals G by XBOOLE_0:def 1;
thus not TS G is empty by A1, Def4; :: thesis: verum