let T be TopSpace; :: thesis: for A being Subset of T holds
( A is 3rd_class iff A ` is 3rd_class )
let A be Subset of T; :: thesis: ( A is 3rd_class iff A ` is 3rd_class )
(Cl (Int A)) ` = Int ((Int A) ` ) by TDLAT_3:4
.= Int (Cl (A ` )) by TDLAT_3:3 ;
then A1: Cl (Int A) = (Int (Cl (A ` ))) ` ;
(Int (Cl A)) ` = Cl ((Cl A) ` ) by TDLAT_3:3
.= Cl (Int (A ` )) by TDLAT_3:4 ;
then A2: Int (Cl A) = (Cl (Int (A ` ))) ` ;
A3: ( A is 3rd_class implies A ` is 3rd_class )

proof

assume A is 3rd_class ; :: thesis: A ` is 3rd_class
then Cl (Int A), Int (Cl A) are_c=-incomparable by Def8;
then ( not Cl (Int A) c= Int (Cl A) & not Int (Cl A) c= Cl (Int A) ) by XBOOLE_0:def 9;
then ( not Cl (Int (A ` )) c= Int (Cl (A ` )) & not Int (Cl (A ` )) c= Cl (Int (A ` )) ) by A1, A2, SUBSET_1:31;
then Cl (Int (A ` )), Int (Cl (A ` )) are_c=-incomparable by XBOOLE_0:def 9;
hence A ` is 3rd_class by Def8; :: thesis: verum

end;

( A ` is 3rd_class implies A is 3rd_class )

proof

assume A ` is 3rd_class ; :: thesis: A is 3rd_class
then Cl (Int (A ` )), Int (Cl (A ` )) are_c=-incomparable by Def8;
then ( not Cl (Int (A ` )) c= Int (Cl (A ` )) & not Int (Cl (A ` )) c= Cl (Int (A ` )) ) by XBOOLE_0:def 9;
then ( not Cl (Int A) c= Int (Cl A) & not Int (Cl A) c= Cl (Int A) ) by A1, A2, SUBSET_1:31;
then Cl (Int A), Int (Cl A) are_c=-incomparable by XBOOLE_0:def 9;
hence A is 3rd_class by Def8; :: thesis: verum

end;

hence ( A is 3rd_class iff A ` is 3rd_class ) by A3; :: thesis: verum