set f = UAp R;
set T = R;
A1: (UAp R) . ({} R) = UAp ({} R) by ROUGHS_2:def 11
.= {} R ;
(UAp R) . ([#] R) = UAp ([#] R) by ROUGHS_2:def 11
.= [#] R by ROUGHS_1:21 ;
then A2: ( UAp R is empty-preserving & UAp R is universe-preserving ) by A1;
for A being Subset of R holds A c= (UAp R) . A
proof
let A be Subset of R; :: thesis: A c= (UAp R) . A
A c= UAp A by ROUGHS_1:13;
hence A c= (UAp R) . A by ROUGHS_2:def 11; :: thesis: verum
end;
then A3: UAp R is extensive ;
for A, B being Subset of R holds (UAp R) . (A \/ B) = ((UAp R) . A) \/ ((UAp R) . B)
proof
let A, B be Subset of R; :: thesis: (UAp R) . (A \/ B) = ((UAp R) . A) \/ ((UAp R) . B)
(UAp R) . (A \/ B) = UAp (A \/ B) by ROUGHS_2:def 11
.= (UAp A) \/ (UAp B) by ROUGHS_1:23
.= ((UAp R) . A) \/ (UAp B) by ROUGHS_2:def 11
.= ((UAp R) . A) \/ ((UAp R) . B) by ROUGHS_2:def 11 ;
hence (UAp R) . (A \/ B) = ((UAp R) . A) \/ ((UAp R) . B) ; :: thesis: verum
end;
then UAp R is \/-preserving ;
hence UAp R is preclosure by A2, A3; :: thesis: verum