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

proof

let X, Y be Element of bool A; :: according to CLOSURE1:def 2 :: thesis: ( X c= Y implies a .. X c= a .. Y )
assume X c= Y ; :: thesis: a .. X c= a .. Y
hence a .. X c= a .. Y by Th9; :: thesis: verum

end;

hence id (bool A) is monotonic MSSetOp of A ; :: thesis: verum