consider x being Chain of f;
x in Chains f by Def17;
hence not Chains f is empty ; :: thesis: verum