let I be set ; :: thesis: for A being ManySortedSet of I holds id (bool A) is topological MSSetOp of A
let A be ManySortedSet of I; :: 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 4 :: thesis: a .. (X (\/) Y) = (a .. X) (\/) (a .. Y)
Y in bool A by MSSUBFAM:12;
then A1: Y c= A by MBOOLEAN:1;
X in bool A by MSSUBFAM:12;
then X c= A by MBOOLEAN:1;
then X (\/) Y c= A by A1, PBOOLE:16;
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