set f = ClMap T;
A1: (ClMap T) . ({} T) = Cl ({} T) by Def15
.= {} T by PRE_TOPC:22 ;
(ClMap T) . ([#] T) = Cl ([#] T) by Def15
.= [#] T by PRE_TOPC:22 ;
hence ( ClMap T is empty-preserving & ClMap T is universe-preserving ) by A1; :: thesis: verum