let I be set ; :: thesis: for M being ManySortedSet of I
for P being MSSetOp of M
for E, T being Element of bool M st P is topological holds
(P .. E) \ (P .. T) c= P .. (E \ T)
let M be ManySortedSet of I; :: thesis: for P being MSSetOp of M
for E, T being Element of bool M st P is topological holds
(P .. E) \ (P .. T) c= P .. (E \ T)
let P be MSSetOp of M; :: thesis: for E, T being Element of bool M st P is topological holds
(P .. E) \ (P .. T) c= P .. (E \ T)
let E, T be Element of bool M; :: thesis: ( P is topological implies (P .. E) \ (P .. T) c= P .. (E \ T) )
E in bool M by MSSUBFAM:12;
then E c= M by MBOOLEAN:1;
then E \ T c= M by MBOOLEAN:15;
then E \ T in bool M by MBOOLEAN:1;
then A1: E \ T is Element of bool M by MSSUBFAM:11;
assume A2: P is topological ; :: thesis: (P .. E) \ (P .. T) c= P .. (E \ T)
then (P .. E) \/ (P .. T) = P .. (E \/ T) by Def5
.= P .. ((E \ T) \/ T) by PBOOLE:67
.= (P .. (E \ T)) \/ (P .. T) by A1, A2, Def5 ;
then P .. E c= (P .. (E \ T)) \/ (P .. T) by PBOOLE:14;
then (P .. E) \ (P .. T) c= ((P .. (E \ T)) \/ (P .. T)) \ (P .. T) by PBOOLE:53;
then A3: (P .. E) \ (P .. T) c= (P .. (E \ T)) \ (P .. T) by PBOOLE:75;
(P .. (E \ T)) \ (P .. T) c= P .. (E \ T) by PBOOLE:56;
hence (P .. E) \ (P .. T) c= P .. (E \ T) by A3, PBOOLE:13; :: thesis: verum