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 ` ))) ) )
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 A1: 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 ( A ` is supercondensed & A ` is subcondensed ) ;
then A2: Cl (Int (A ` )) = Cl (A ` ) by Def2;
( A is supercondensed & A is subcondensed ) by A1;
then ( Int (Cl A) = Int A & Cl (Int A) = Cl A ) by Def1, Def2;
hence ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A ` ))) ) by A2, TOPS_1:def 2; :: thesis: verum

end;

assume A3: ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A ` ))) ) ; :: thesis: A is condensed
A4: Int A c= A by TOPS_1:44;
A5: A c= Cl A by PRE_TOPC:48;
(Cl A) \/ (Int A) = (Int A) \/ (Fr A) by XBOOLE_1:39;
then A6: Cl A = (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A ` )))) by A3, A4, A5, XBOOLE_1:1, XBOOLE_1:12;
(Cl (Int A)) /\ (Cl (Int (A ` ))) c= Cl (Int A) by XBOOLE_1:17;
then (Int A) \/ ((Cl (Int A)) /\ (Cl (Int (A ` )))) c= (Int A) \/ (Cl (Int A)) by XBOOLE_1:13;
then A7: Cl A c= Cl (Int A) by A6, PRE_TOPC:48, XBOOLE_1:12;
Cl (Int A) c= Cl A by PRE_TOPC:49, TOPS_1:44;
then Cl (Int A) = Cl A by A7, XBOOLE_0:def 10;
then A8: A is subcondensed by Def2;
A9: Int (A ` ) c= A ` by TOPS_1:44;
A10: A ` c= Cl (A ` ) by PRE_TOPC:48;
A11: Cl (Int (A ` )) c= Cl (A ` ) by PRE_TOPC:49, TOPS_1:44;
A12: Fr A = Fr (A ` ) by TOPS_1:62;
(Cl (A ` )) \/ (Int (A ` )) = (Int (A ` )) \/ (Fr (A ` )) by XBOOLE_1:39;
then A13: Cl (A ` ) = (Int (A ` )) \/ ((Cl (Int (A ` ))) /\ (Cl (Int ((A ` ) ` )))) by A3, A9, A10, A12, XBOOLE_1:1, XBOOLE_1:12;
(Cl (Int (A ` ))) /\ (Cl (Int ((A ` ) ` ))) c= Cl (Int (A ` )) by XBOOLE_1:17;
then A14: (Int (A ` )) \/ ((Cl (Int (A ` ))) /\ (Cl (Int ((A ` ) ` )))) c= (Int (A ` )) \/ (Cl (Int (A ` ))) by XBOOLE_1:13;
(Int (A ` )) \/ (Cl (Int (A ` ))) = Cl (Int (A ` )) by PRE_TOPC:48, XBOOLE_1:12;
then A15: Cl (A ` ) = Cl (Int (A ` )) by A11, A13, A14, XBOOLE_0:def 10;
A16: Cl (A ` ) = (Int A) ` by TDLAT_3:3;
Cl (Int (A ` )) = Cl ((Cl A) ` ) by TDLAT_3:4
.= (Int (Cl A)) ` by TDLAT_3:3 ;
then Int A = ((Int (Cl A)) ` ) ` by A15, A16;
then A is supercondensed by Def1;
hence A is condensed by A8; :: thesis: verum