set f = UAp R;
A: UAp R is preclosure ;
UAp R is idempotent

proof

for A being Subset of R holds (UAp R) . A = (UAp R) . ((UAp R) . A)

proof

let A be Subset of R; :: thesis: (UAp R) . A = (UAp R) . ((UAp R) . A)
(UAp R) . A = UAp A by ROUGHS_2:def 11
.= UAp (UAp A) by ROUGHS_1:35
.= (UAp R) . (UAp A) by ROUGHS_2:def 11
.= (UAp R) . ((UAp R) . A) by ROUGHS_2:def 11 ;
hence (UAp R) . A = (UAp R) . ((UAp R) . A) ; :: thesis: verum

end;

hence UAp R is idempotent ; :: thesis: verum

end;

hence UAp R is closure by A; :: thesis: verum