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