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

proof

let X be Element of Bool A; :: according to CLOSURE2:def 14 :: thesis: f . X = f . (f . X)
thus f . (f . X) = f . X by FUNCT_1:35; :: thesis: verum

end;

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