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)
.= P .. ((E (\) T) (\/) T) by PBOOLE:67
.= (P .. (E (\) T)) (\/) (P .. T) by A1, A2 ;
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