let I be set ; :: thesis: for A being ManySortedSet of holds id (bool A) is idempotent MSSetOp of A
let A be ManySortedSet of ; :: thesis: id (bool A) is idempotent MSSetOp of A
reconsider a = id (bool A) as MSSetOp of A ;
a is idempotent

proof

let X be Element of bool A; :: according to CLOSURE1:def 4 :: thesis: a .. X = a .. (a .. X)
thus a .. X = a .. (a .. X) by Th8; :: thesis: verum

end;

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