f . {} = {} by Def12;
hence Flip f is universe-preserving by Th18; :: thesis: verum