set f = LAp R;
set T = R;
A1: (LAp R) . ({} R) = LAp ({} R) by ROUGHS_2:def 10
.= {} R by ROUGHS_1:18 ;
(LAp R) . ([#] R) = LAp ([#] R) by ROUGHS_2:def 10
.= [#] R ;
then A2: ( LAp R is empty-preserving & LAp R is universe-preserving ) by A1;
for A being Subset of R holds (LAp R) . A c= A

proof

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

end;

then A3: LAp R is intensive ;
for A, B being Subset of R holds (LAp R) . (A /\ B) = ((LAp R) . A) /\ ((LAp R) . B)

proof

let A, B be Subset of R; :: thesis: (LAp R) . (A /\ B) = ((LAp R) . A) /\ ((LAp R) . B)
(LAp R) . (A /\ B) = LAp (A /\ B) by ROUGHS_2:def 10
.= (LAp A) /\ (LAp B) by ROUGHS_1:22
.= ((LAp R) . A) /\ (LAp B) by ROUGHS_2:def 10
.= ((LAp R) . A) /\ ((LAp R) . B) by ROUGHS_2:def 10 ;
hence (LAp R) . (A /\ B) = ((LAp R) . A) /\ ((LAp R) . B) ; :: thesis: verum

end;

then LAp R is /\-preserving ;
hence LAp R is preinterior by A2, A3; :: thesis: verum