let T be TopSpace; :: thesis: for A being Subset of T holds
( A is 1st_class iff A ` is 1st_class )
let A be Subset of T; :: thesis: ( A is 1st_class iff A ` is 1st_class )
A1: ( A is 1st_class implies A ` is 1st_class )

proof

assume A is 1st_class ; :: thesis: A ` is 1st_class
then Int (Cl A) c= Cl (Int A) by Def6;
then (Cl (Int A)) ` c= (Int (Cl A)) ` by SUBSET_1:31;
then Int ((Int A) ` ) c= (Int (Cl A)) ` by TDLAT_3:4;
then Int ((Int A) ` ) c= Cl ((Cl A) ` ) by TDLAT_3:3;
then Int ((Int A) ` ) c= Cl (Int (A ` )) by TDLAT_3:4;
then Int (Cl (A ` )) c= Cl (Int (A ` )) by TDLAT_3:3;
hence A ` is 1st_class by Def6; :: thesis: verum

end;

( A ` is 1st_class implies A is 1st_class )

proof

assume A ` is 1st_class ; :: thesis: A is 1st_class
then Int (Cl (A ` )) c= Cl (Int (A ` )) by Def6;
then Int ((Int A) ` ) c= Cl (Int (A ` )) by TDLAT_3:3;
then (Cl (Int A)) ` c= Cl (Int (A ` )) by TDLAT_3:4;
then (Cl (Int A)) ` c= Cl ((Cl A) ` ) by TDLAT_3:4;
then (Cl (Int A)) ` c= (Int (Cl A)) ` by TDLAT_3:3;
then Int (Cl A) c= Cl (Int A) by SUBSET_1:31;
hence A is 1st_class by Def6; :: thesis: verum

end;

hence ( A is 1st_class iff A ` is 1st_class ) by A1; :: thesis: verum