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 )
(Int (Cl A)) ` = Cl ((Cl A) ` ) by TDLAT_3:3
.= Cl (Int (A ` )) by TDLAT_3:4 ;
then A1: Int (Cl A) = (Cl (Int (A ` ))) ` ;
(Cl (Int A)) ` = Int ((Int A) ` ) by TDLAT_3:4
.= Int (Cl (A ` )) by TDLAT_3:3 ;
then A2: Cl (Int A) = (Int (Cl (A ` ))) ` ;
A3: ( A ` is 3rd_class implies A is 3rd_class )

proof

assume A ` is 3rd_class ; :: thesis: A is 3rd_class
then A4: Cl (Int (A ` )), Int (Cl (A ` )) are_c=-incomparable by Def8;
then not Int (Cl (A ` )) c= Cl (Int (A ` )) by XBOOLE_0:def 9;
then A5: not Int (Cl A) c= Cl (Int A) by A2, A1, SUBSET_1:31;
not Cl (Int (A ` )) c= Int (Cl (A ` )) by A4, XBOOLE_0:def 9;
then not Cl (Int A) c= Int (Cl A) by A2, A1, SUBSET_1:31;
then Cl (Int A), Int (Cl A) are_c=-incomparable by A5, 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 A6: Cl (Int A), Int (Cl A) are_c=-incomparable by Def8;
then not Int (Cl A) c= Cl (Int A) by XBOOLE_0:def 9;
then A7: not Int (Cl (A ` )) c= Cl (Int (A ` )) by A2, A1, SUBSET_1:31;
not Cl (Int A) c= Int (Cl A) by A6, XBOOLE_0:def 9;
then not Cl (Int (A ` )) c= Int (Cl (A ` )) by A2, A1, SUBSET_1:31;
then Cl (Int (A ` )), Int (Cl (A ` )) are_c=-incomparable by A7, 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