let A be Subset of T; :: thesis: ( A is 1st_class implies ( not A is 2nd_class & not A is 3rd_class ) )
assume A is 1st_class ; :: thesis: ( not A is 2nd_class & not A is 3rd_class )
then A1: Int (Cl A) c= Cl (Int A) by Def6;
then A2: not Cl (Int A) c< Int (Cl A) by XBOOLE_1:60;
Cl (Int A), Int (Cl A) are_c=-comparable by A1, XBOOLE_0:def 9;
hence ( not A is 2nd_class & not A is 3rd_class ) by A2, Def7, Def8; :: thesis: verum