ex t being set st t in Terminals G by XBOOLE_0:def 1;
hence not TS G is empty by Def4; :: thesis: verum