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

proof

let X, Y be Element of Bool A; :: according to CLOSURE2:def 11 :: thesis: ( X c=' Y implies f . X c=' f . Y )
assume A1: X c= Y ; :: thesis: f . X c=' f . Y
f . X = X by FUNCT_1:18;
hence f . X c=' f . Y by A1, FUNCT_1:18; :: thesis: verum

end;

hence id (Bool A) is monotonic SetOp of A ; :: thesis: verum