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:48;
(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 ` ) by Def2;
Cl (Int A) = Cl A by A3, Def2;
hence ( Fr A = (Cl (Int A)) \ (Int (Cl A)) & Fr A = (Cl (Int A)) /\ (Cl (Int (A ` ))) ) by A3, A4, Def1, 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:44;
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: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: A ` c= Cl (A ` ) by PRE_TOPC:48;
A10: (Cl (A ` )) \/ (Int (A ` )) = (Int (A ` )) \/ (Fr (A ` )) by XBOOLE_1:39;
A11: Fr A = Fr (A ` ) by TOPS_1:62;
(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:49, TOPS_1:44;
A14: Cl (Int (A ` )) = Cl ((Cl A) ` ) by TDLAT_3:4
.= (Int (Cl A)) ` by TDLAT_3:3 ;
A15: (Int (A ` )) \/ (Cl (Int (A ` ))) = Cl (Int (A ` )) by PRE_TOPC:48, XBOOLE_1:12;
Int (A ` ) c= A ` by TOPS_1:44;
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:3;
then Int A = ((Int (Cl A)) ` ) ` by A16, A14;
then A is supercondensed by Def1;
hence A is condensed by A8; :: thesis: verum