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