set U = T * ;
reconsider T = T as Subset of (T *) by Th9;
take T ; :: thesis: ( not T is empty & T is antichain-like )
thus ( not T is empty & T is antichain-like ) ; :: thesis: verum