let I be set ; :: thesis: for A being ManySortedSet of I holds id (Bool A) is monotonic SetOp of A
let A be ManySortedSet of I; :: thesis: id (Bool A) is monotonic SetOp of A
reconsider f = id (Bool A) as SetOp of A ;
f is monotonic ;
hence id (Bool A) is monotonic SetOp of A ; :: thesis: verum