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 13 :: thesis: f . (X (\/) Y) = (f . X) (\/) (f . Y)
( X c= A & Y c= A ) by PBOOLE:def 18;
then X (\/) Y c= A by PBOOLE:16;
then X (\/) Y is ManySortedSubset of A by PBOOLE:def 18;
then X (\/) Y in Bool A by Def1;
hence f . (X (\/) Y) = X (\/) Y by FUNCT_1:18
.= (f . X) (\/) Y
.= (f . X) (\/) (f . Y) ;
:: thesis: verum
end;
hence id (Bool A) is topological SetOp of A ; :: thesis: verum