Cl {x} = downarrow x by Th22;
hence downarrow x is closed ; :: thesis: verum