consider x being Element of T;
consider A being non empty proper Subset of T;
reconsider A = {x} as Subset of T ;
Cl A = the carrier of T by TEX_1:11;
hence ex b₁ being Subset of T st b₁ is 2nd_class ; :: thesis: verum