set a = the Element of T;
reconsider A = { the Element of T} as Subset of T ;
set X = NAT --> A;
reconsider X = NAT --> A as SetSequence of T ;
take X ; :: thesis: X is non-empty
thus X is non-empty ; :: thesis: verum