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

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

hence
id (bool A) is topological MSSetOp of A
; :: thesis: verum
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;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