LAp (UAp A) = UAp (UAp A) by ROUGHS_1:36
.= UAp A ;
hence Cl A is open ; :: thesis: verum