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) by Def15
.= g . ((E \ T) \/ T) by PBOOLE:73
.= (g . A) \/ (g . T) by A1, A2, Def15 ;
then g . E c= (g . A) \/ (g . T) by PBOOLE:16;
then (g . E) \ (g . T) c= ((g . A) \/ (g . T)) \ (g . T) by PBOOLE:59;
then A3: (g . E) \ (g . T) c= (g . A) \ (g . T) by PBOOLE:81;
(g . A) \ (g . T) c= g . A by PBOOLE:62;
hence (g . E) \ (g . T) c= g . A by A3, PBOOLE:15; :: thesis: verum