take f = id S; :: thesis: f is idempotent
f * f = f by FUNCT_2:17;
hence f is idempotent by QUANTAL1:def 9; :: thesis: verum