let I be set ; :: thesis: for A being ManySortedSet of I holds id (bool A) is idempotent MSSetOp of A
let A be ManySortedSet of I; :: thesis: id (bool A) is idempotent MSSetOp of A
reconsider a = id (bool A) as MSSetOp of A ;
a is idempotent by Th8;
hence id (bool A) is idempotent MSSetOp of A ; :: thesis: verum