{} c= A ;
hence not Fin A is empty by Def5; :: thesis: verum