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:2
.= Cl (Int (A `)) by TDLAT_3:3 ;
then A1: Int (Cl A) = (Cl (Int (A `))) ` ;
(Cl (Int A)) ` = Int ((Int A) `) by TDLAT_3:3
.= Int (Cl (A `)) by TDLAT_3:2 ;
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 ;
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:12;
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:12;
then Cl (Int A), Int (Cl A) are_c=-incomparable by A5, XBOOLE_0:def 9;
hence A is 3rd_class ; :: 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 ;
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:12;
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:12;
then Cl (Int (A `)), Int (Cl (A `)) are_c=-incomparable by A7, XBOOLE_0:def 9;
hence A ` is 3rd_class ; :: thesis: verum

end;

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