let I be set ; :: thesis: for M being ManySortedSet of I
for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E (\) T & g is topological holds
(g . E) (\) (g . T) c= g . A
let M be ManySortedSet of I; :: thesis: for E, T being Element of Bool M
for g being SetOp of M
for A being Element of Bool M st A = E (\) T & g is topological holds
(g . E) (\) (g . T) c= g . A
let E, T be Element of Bool M; :: thesis: for g being SetOp of M
for A being Element of Bool M st A = E (\) T & g is topological holds
(g . E) (\) (g . T) c= g . A
let g be SetOp of M; :: thesis: for A being Element of Bool M st A = E (\) T & g is topological holds
(g . E) (\) (g . T) c= g . A
let A be Element of Bool M; :: thesis: ( A = E (\) T & g is topological implies (g . E) (\) (g . T) c= g . A )
assume A1: A = E (\) T ; :: thesis: ( not g is topological or (g . E) (\) (g . T) c= g . A )
assume A2: g is topological ; :: thesis: (g . E) (\) (g . T) c= g . A
then (g . E) (\/) (g . T) = g . (E (\/) T)
.= g . ((E (\) T) (\/) T) by PBOOLE:67
.= (g . A) (\/) (g . T) by A1, A2 ;
then g . E c= (g . A) (\/) (g . T) by PBOOLE:14;
then (g . E) (\) (g . T) c= ((g . A) (\/) (g . T)) (\) (g . T) by PBOOLE:53;
then A3: (g . E) (\) (g . T) c= (g . A) (\) (g . T) by PBOOLE:75;
(g . A) (\) (g . T) c= g . A by PBOOLE:56;
hence (g . E) (\) (g . T) c= g . A by A3, PBOOLE:13; :: thesis: verum