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 that
A1: not A is 1st_class and
A2: not A is 2nd_class and
A3: not A is 3rd_class ; :: thesis: contradiction
A4: not Cl (Int A) c< Int (Cl A) by A2, Def7;
A5: Cl (Int A), Int (Cl A) are_c=-comparable by A3, Def8;
not Int (Cl A) c= Cl (Int A) by A1, Def6;
hence contradiction by A4, A5, Th45; :: thesis: verum