thus ( A is dense implies Cl A = the carrier of X ) :: thesis: ( Cl A = the carrier of X implies A is dense )
proof
assume A is dense ; :: thesis: Cl A = the carrier of X
then Cl A = [#] X by TOPS_1:def 3;
hence Cl A = the carrier of X ; :: thesis: verum
end;
assume Cl A = the carrier of X ; :: thesis: A is dense
then Cl A = [#] X ;
hence A is dense by TOPS_1:def 3; :: thesis: verum