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