set f = LAp R;
A: LAp R is preinterior ;
LAp R is idempotent

proof

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

proof

let A be Subset of R; :: thesis: (LAp R) . A = (LAp R) . ((LAp R) . A)
(LAp R) . A = LAp A by ROUGHS_2:def 10
.= LAp (LAp A) by ROUGHS_1:33
.= (LAp R) . (LAp A) by ROUGHS_2:def 10
.= (LAp R) . ((LAp R) . A) by ROUGHS_2:def 10 ;
hence (LAp R) . A = (LAp R) . ((LAp R) . A) ; :: thesis: verum

end;

hence LAp R is idempotent ; :: thesis: verum

end;

hence LAp R is interior by A; :: thesis: verum