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