let A be Subset of T; :: thesis: ( A is proper & not A is empty implies A is 2nd_class )
assume A1: ( A is proper & not A is empty ) ; :: thesis: A is 2nd_class
then A <> the carrier of T ;
then Int A = {} by TEX_1:10;
then A2: Cl (Int A) = {} by TEX_1:9;
Cl A = the carrier of T by A1, TEX_1:9;
then Int (Cl A) = the carrier of T by TEX_1:10;
then Cl (Int A) c< Int (Cl A) by A2, XBOOLE_0:def 8;
hence A is 2nd_class ; :: thesis: verum