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 )

( 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

( A is 1st_class implies A ` is 1st_class )
assume
A ` is 1st_class
; :: thesis: A is 1st_class

then Int (Cl (A `)) c= Cl (Int (A `)) ;

then Int ((Int A) `) c= Cl (Int (A `)) by TDLAT_3:2;

then (Cl (Int A)) ` c= Cl (Int (A `)) by TDLAT_3:3;

then (Cl (Int A)) ` c= Cl ((Cl A) `) by TDLAT_3:3;

then (Cl (Int A)) ` c= (Int (Cl A)) ` by TDLAT_3:2;

then Int (Cl A) c= Cl (Int A) by SUBSET_1:12;

hence A is 1st_class ; :: thesis: verum

end;then Int (Cl (A `)) c= Cl (Int (A `)) ;

then Int ((Int A) `) c= Cl (Int (A `)) by TDLAT_3:2;

then (Cl (Int A)) ` c= Cl (Int (A `)) by TDLAT_3:3;

then (Cl (Int A)) ` c= Cl ((Cl A) `) by TDLAT_3:3;

then (Cl (Int A)) ` c= (Int (Cl A)) ` by TDLAT_3:2;

then Int (Cl A) c= Cl (Int A) by SUBSET_1:12;

hence A is 1st_class ; :: thesis: verum

proof

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

then Int (Cl A) c= Cl (Int A) ;

then (Cl (Int A)) ` c= (Int (Cl A)) ` by SUBSET_1:12;

then Int ((Int A) `) c= (Int (Cl A)) ` by TDLAT_3:3;

then Int ((Int A) `) c= Cl ((Cl A) `) by TDLAT_3:2;

then Int ((Int A) `) c= Cl (Int (A `)) by TDLAT_3:3;

then Int (Cl (A `)) c= Cl (Int (A `)) by TDLAT_3:2;

hence A ` is 1st_class ; :: thesis: verum

end;then Int (Cl A) c= Cl (Int A) ;

then (Cl (Int A)) ` c= (Int (Cl A)) ` by SUBSET_1:12;

then Int ((Int A) `) c= (Int (Cl A)) ` by TDLAT_3:3;

then Int ((Int A) `) c= Cl ((Cl A) `) by TDLAT_3:2;

then Int ((Int A) `) c= Cl (Int (A `)) by TDLAT_3:3;

then Int (Cl (A `)) c= Cl (Int (A `)) by TDLAT_3:2;

hence A ` is 1st_class ; :: thesis: verum