set x = the Chain of f;
the Chain of f in Chains f by Def13;
hence not Chains f is empty ; :: thesis: verum