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