0 <= (@ f) . x by FUZZY_2:1;
hence f . x is Element of ; :: thesis: verum