the Sorts of C . the bool-sort of S = BOOLEAN by AOFA_A00:def 32;
hence t value_at (C,u) is boolean ; :: thesis: verum