thus ( A is everywhere_dense implies Cl (Int A) = the carrier of X ) :: thesis: ( Cl (Int A) = the carrier of X implies A is everywhere_dense )

proof

assume A is everywhere_dense ; :: thesis: Cl (Int A) = the carrier of X
then Cl (Int A) = [#] X by Def4;
hence Cl (Int A) = the carrier of X ; :: thesis: verum

end;

assume Cl (Int A) = the carrier of X ; :: thesis: A is everywhere_dense
then Cl (Int A) = [#] X ;
hence A is everywhere_dense by Def4; :: thesis: verum