set f = IntMap T;
A1: (IntMap T) . ({} T) = Int ({} T) by ROUGHS_2:def 16
.= {} T ;
(IntMap T) . ([#] T) = Int ([#] T) by ROUGHS_2:def 16
.= [#] T by TOPS_1:15 ;
then A2: ( IntMap T is empty-preserving & IntMap T is universe-preserving ) by A1;
for A being Subset of T holds (IntMap T) . A c= A

proof

let A be Subset of T; :: thesis: (IntMap T) . A c= A
Int A c= A by TOPS_1:16;
hence (IntMap T) . A c= A by ROUGHS_2:def 16; :: thesis: verum

end;

then A3: IntMap T is intensive ;
A4: IntMap T is idempotent

proof

for A being Subset of T holds (IntMap T) . A = (IntMap T) . ((IntMap T) . A)

proof

let A be Subset of T; :: thesis: (IntMap T) . A = (IntMap T) . ((IntMap T) . A)
(IntMap T) . A = Int (Int A) by ROUGHS_2:def 16
.= (IntMap T) . (Int A) by ROUGHS_2:def 16
.= (IntMap T) . ((IntMap T) . A) by ROUGHS_2:def 16 ;
hence (IntMap T) . A = (IntMap T) . ((IntMap T) . A) ; :: thesis: verum

end;

hence IntMap T is idempotent ; :: thesis: verum

end;

for A, B being Subset of T holds (IntMap T) . (A /\ B) = ((IntMap T) . A) /\ ((IntMap T) . B)

proof

let A, B be Subset of T; :: thesis: (IntMap T) . (A /\ B) = ((IntMap T) . A) /\ ((IntMap T) . B)
(IntMap T) . (A /\ B) = Int (A /\ B) by ROUGHS_2:def 16
.= (Int A) /\ (Int B) by TOPS_1:17
.= ((IntMap T) . A) /\ (Int B) by ROUGHS_2:def 16
.= ((IntMap T) . A) /\ ((IntMap T) . B) by ROUGHS_2:def 16 ;
hence (IntMap T) . (A /\ B) = ((IntMap T) . A) /\ ((IntMap T) . B) ; :: thesis: verum

end;

then IntMap T is /\-preserving ;
hence IntMap T is interior by A2, A3, A4; :: thesis: verum