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 )

( 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

( A is 3rd_class implies A ` is 3rd_class )
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;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

proof

hence
( A is 3rd_class iff A ` is 3rd_class )
by A3; :: thesis: verum
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;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