UAp (LAp A) = LAp (LAp A) by ROUGHS_1:34
.= LAp A ;
hence Int A is closed ; :: thesis: verum