let T be TopSpace; :: thesis: for A being Subset of T holds

( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) )

let A be Subset of T; :: thesis: ( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) )

A1: A c= Cl A by PRE_TOPC:18;

(Cl (Int A)) /\ (Cl (Int (A `))) c= Cl (Int A) by XBOOLE_1:17;

then A2: (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A `)))) c= (Int A) \/ (Cl (Int A)) by XBOOLE_1:13;

thus ( A is condensed implies ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) ) :: thesis: ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) implies A is condensed )

Fr A = (Cl (Int A)) \ (Int (Cl A)) and

A5: Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ; :: thesis: A is condensed

A6: (Cl A) \/ (Int A) = (Int A) \/ (Fr A) by XBOOLE_1:39;

Int A c= A by TOPS_1:16;

then Cl A = (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A `)))) by A5, A1, A6, XBOOLE_1:1, XBOOLE_1:12;

then A7: Cl A c= Cl (Int A) by A2, PRE_TOPC:18, XBOOLE_1:12;

Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;

then Cl (Int A) = Cl A by A7, XBOOLE_0:def 10;

then A8: A is subcondensed ;

A9: A ` c= Cl (A `) by PRE_TOPC:18;

A10: (Cl (A `)) \/ (Int (A `)) = (Int (A `)) \/ (Fr (A `)) by XBOOLE_1:39;

A11: Fr A = Fr (A `) by TOPS_1:29;

(Cl (Int (A `))) /\ (Cl (Int ((A `) `))) c= Cl (Int (A `)) by XBOOLE_1:17;

then A12: (Int (A `)) \/ ((Cl (Int (A `))) /\ (Cl (Int ((A `) `)))) c= (Int (A `)) \/ (Cl (Int (A `))) by XBOOLE_1:13;

A13: Cl (Int (A `)) c= Cl (A `) by PRE_TOPC:19, TOPS_1:16;

A14: Cl (Int (A `)) = Cl ((Cl A) `) by TDLAT_3:3

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

A15: (Int (A `)) \/ (Cl (Int (A `))) = Cl (Int (A `)) by PRE_TOPC:18, XBOOLE_1:12;

Int (A `) c= A ` by TOPS_1:16;

then Cl (A `) = (Int (A `)) \/ ((Cl (Int (A `))) /\ (Cl (Int ((A `) `)))) by A5, A9, A11, A10, XBOOLE_1:1, XBOOLE_1:12;

then A16: Cl (A `) = Cl (Int (A `)) by A13, A12, A15, XBOOLE_0:def 10;

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

then Int A = ((Int (Cl A)) `) ` by A16, A14;

then A is supercondensed ;

hence A is condensed by A8; :: thesis: verum

( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) )

let A be Subset of T; :: thesis: ( A is condensed iff ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) )

A1: A c= Cl A by PRE_TOPC:18;

(Cl (Int A)) /\ (Cl (Int (A `))) c= Cl (Int A) by XBOOLE_1:17;

then A2: (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A `)))) c= (Int A) \/ (Cl (Int A)) by XBOOLE_1:13;

thus ( A is condensed implies ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) ) :: thesis: ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) implies A is condensed )

proof

assume that
assume A3:
A is condensed
; :: thesis: ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) )

then A ` is condensed by TDLAT_1:16;

then A4: Cl (Int (A `)) = Cl (A `) ;

thus ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) by A3, A4, TOPS_1:def 2; :: thesis: verum

end;then A ` is condensed by TDLAT_1:16;

then A4: Cl (Int (A `)) = Cl (A `) ;

thus ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ) by A3, A4, TOPS_1:def 2; :: thesis: verum

Fr A = (Cl (Int A)) \ (Int (Cl A)) and

A5: Fr A = (Cl (Int A)) /\ (Cl (Int (A `))) ; :: thesis: A is condensed

A6: (Cl A) \/ (Int A) = (Int A) \/ (Fr A) by XBOOLE_1:39;

Int A c= A by TOPS_1:16;

then Cl A = (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A `)))) by A5, A1, A6, XBOOLE_1:1, XBOOLE_1:12;

then A7: Cl A c= Cl (Int A) by A2, PRE_TOPC:18, XBOOLE_1:12;

Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;

then Cl (Int A) = Cl A by A7, XBOOLE_0:def 10;

then A8: A is subcondensed ;

A9: A ` c= Cl (A `) by PRE_TOPC:18;

A10: (Cl (A `)) \/ (Int (A `)) = (Int (A `)) \/ (Fr (A `)) by XBOOLE_1:39;

A11: Fr A = Fr (A `) by TOPS_1:29;

(Cl (Int (A `))) /\ (Cl (Int ((A `) `))) c= Cl (Int (A `)) by XBOOLE_1:17;

then A12: (Int (A `)) \/ ((Cl (Int (A `))) /\ (Cl (Int ((A `) `)))) c= (Int (A `)) \/ (Cl (Int (A `))) by XBOOLE_1:13;

A13: Cl (Int (A `)) c= Cl (A `) by PRE_TOPC:19, TOPS_1:16;

A14: Cl (Int (A `)) = Cl ((Cl A) `) by TDLAT_3:3

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

A15: (Int (A `)) \/ (Cl (Int (A `))) = Cl (Int (A `)) by PRE_TOPC:18, XBOOLE_1:12;

Int (A `) c= A ` by TOPS_1:16;

then Cl (A `) = (Int (A `)) \/ ((Cl (Int (A `))) /\ (Cl (Int ((A `) `)))) by A5, A9, A11, A10, XBOOLE_1:1, XBOOLE_1:12;

then A16: Cl (A `) = Cl (Int (A `)) by A13, A12, A15, XBOOLE_0:def 10;

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

then Int A = ((Int (Cl A)) `) ` by A16, A14;

then A is supercondensed ;

hence A is condensed by A8; :: thesis: verum