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

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