let A be Subset of T; :: thesis: ( A is 2nd_class implies ( not A is 1st_class & not A is 3rd_class ) )

assume A is 2nd_class ; :: thesis: ( not A is 1st_class & not A is 3rd_class )

then A1: Cl (Int A) c< Int (Cl A) ;

then Cl (Int A) c= Int (Cl A) by XBOOLE_0:def 8;

then A2: Cl (Int A), Int (Cl A) are_c=-comparable by XBOOLE_0:def 9;

not Int (Cl A) c= Cl (Int A) by A1, XBOOLE_0:def 8;

hence ( not A is 1st_class & not A is 3rd_class ) by A2; :: thesis: verum

assume A is 2nd_class ; :: thesis: ( not A is 1st_class & not A is 3rd_class )

then A1: Cl (Int A) c< Int (Cl A) ;

then Cl (Int A) c= Int (Cl A) by XBOOLE_0:def 8;

then A2: Cl (Int A), Int (Cl A) are_c=-comparable by XBOOLE_0:def 9;

not Int (Cl A) c= Cl (Int A) by A1, XBOOLE_0:def 8;

hence ( not A is 1st_class & not A is 3rd_class ) by A2; :: thesis: verum