let T be TopSpace; :: thesis: Flip (IntMap T) = ClMap T
Flip (Flip (ClMap T)) = Flip (IntMap T) by Th25;
hence Flip (IntMap T) = ClMap T by Th23; :: thesis: verum