f . A = A by Def13;
hence Flip f is empty-preserving by Th19; :: thesis: verum