let T be TopSpace; :: thesis: for A being Subset of T holds
( A is 1st_class or A is 2nd_class or A is 3rd_class )
let A be Subset of T; :: thesis: ( A is 1st_class or A is 2nd_class or A is 3rd_class )
assume ( not A is 1st_class & not A is 2nd_class & not A is 3rd_class ) ; :: thesis: contradiction
then ( not Int (Cl A) c= Cl (Int A) & not Cl (Int A) c< Int (Cl A) & Cl (Int A), Int (Cl A) are_c=-comparable ) by Def6, Def7, Def8;
hence contradiction by Th45; :: thesis: verum