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

proof

let X, Y be Element of bool A; :: according to CLOSURE1:def 5 :: thesis: a .. (X \/ Y) = (a .. X) \/ (a .. Y)
( X in bool A & Y in bool A ) by MSSUBFAM:12;
then ( X c= A & Y c= A ) by MBOOLEAN:1;
then X \/ Y c= A by PBOOLE:18;
then X \/ Y in bool A by MBOOLEAN:1;
then X \/ Y is Element of bool A by MSSUBFAM:11;
hence a .. (X \/ Y) = (a .. X) \/ (a .. Y) by Th10; :: thesis: verum

end;

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