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

proof

let X, Y be Element of Bool A; :: according to CLOSURE2:def 15 :: thesis: f . (X \/ Y) = (f . X) \/ (f . Y)
( X c= A & Y c= A ) by PBOOLE:def 23;
then X \/ Y c= A by PBOOLE:18;
then X \/ Y is ManySortedSubset of A by PBOOLE:def 23;
then X \/ Y in Bool A by Def1;
hence f . (X \/ Y) = X \/ Y by FUNCT_1:35
.= (f . X) \/ Y by FUNCT_1:35
.= (f . X) \/ (f . Y) by FUNCT_1:35 ;
:: thesis: verum

end;

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