let T be TopSpace; :: thesis: for A being Subset of T holds
( A is 2nd_class iff A ` is 2nd_class )
let A be Subset of T; :: thesis: ( A is 2nd_class iff A ` is 2nd_class )
A1: for A being Subset of T st A ` is 2nd_class holds
A is 2nd_class

proof

let A be Subset of T; :: thesis: ( A ` is 2nd_class implies A is 2nd_class )
assume A ` is 2nd_class ; :: thesis: A is 2nd_class
then Cl (Int (A ` )) c< Int (Cl (A ` )) by Def7;
then ( Cl (Int (A ` )) c= Int (Cl (A ` )) & Cl (Int (A ` )) <> Int (Cl (A ` )) ) by XBOOLE_0:def 8;
then ( Cl (Int (A ` )) c= Int ((Int A) ` ) & Cl ((Cl A) ` ) <> Int (Cl (A ` )) ) by TDLAT_3:3, TDLAT_3:4;
then ( Cl (Int (A ` )) c= (Cl (Int A)) ` & Cl ((Cl A) ` ) <> Int ((Int A) ` ) ) by TDLAT_3:3, TDLAT_3:4;
then ( Cl ((Cl A) ` ) c= (Cl (Int A)) ` & (Cl (Int A)) ` <> Cl ((Cl A) ` ) ) by TDLAT_3:4;
then ( (Int (Cl A)) ` c= (Cl (Int A)) ` & Cl (Int A) <> Int (Cl A) ) by TDLAT_3:3;
then ( Cl (Int A) c= Int (Cl A) & Cl (Int A) <> Int (Cl A) ) by SUBSET_1:31;
then Cl (Int A) c< Int (Cl A) by XBOOLE_0:def 8;
hence A is 2nd_class by Def7; :: thesis: verum

end;

( A is 2nd_class implies A ` is 2nd_class )

proof

assume A is 2nd_class ; :: thesis: A ` is 2nd_class
then (A ` ) ` is 2nd_class ;
hence A ` is 2nd_class by A1; :: thesis: verum

end;

hence ( A is 2nd_class iff A ` is 2nd_class ) by A1; :: thesis: verum