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

( 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

( A is 2nd_class implies A ` is 2nd_class )
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 A2: Cl (Int (A `)) c< Int (Cl (A `)) ;

then Cl (Int (A `)) c= Int (Cl (A `)) by XBOOLE_0:def 8;

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

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

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

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

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

Cl ((Cl A) `) <> Int (Cl (A `)) by A2, TDLAT_3:3;

then Cl ((Cl A) `) <> Int ((Int A) `) by TDLAT_3:2;

then (Cl (Int A)) ` <> Cl ((Cl A) `) by TDLAT_3:3;

then Cl (Int A) <> Int (Cl A) by TDLAT_3:2;

then Cl (Int A) c< Int (Cl A) by A3, XBOOLE_0:def 8;

hence A is 2nd_class ; :: thesis: verum

end;assume A ` is 2nd_class ; :: thesis: A is 2nd_class

then A2: Cl (Int (A `)) c< Int (Cl (A `)) ;

then Cl (Int (A `)) c= Int (Cl (A `)) by XBOOLE_0:def 8;

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

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

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

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

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

Cl ((Cl A) `) <> Int (Cl (A `)) by A2, TDLAT_3:3;

then Cl ((Cl A) `) <> Int ((Int A) `) by TDLAT_3:2;

then (Cl (Int A)) ` <> Cl ((Cl A) `) by TDLAT_3:3;

then Cl (Int A) <> Int (Cl A) by TDLAT_3:2;

then Cl (Int A) c< Int (Cl A) by A3, XBOOLE_0:def 8;

hence A is 2nd_class ; :: thesis: verum

proof

hence
( A is 2nd_class iff A ` is 2nd_class )
by A1; :: thesis: verum
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;then (A `) ` is 2nd_class ;

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