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 )
proof
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;
assume that
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