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 monotonic holds
g . A c= (g . E) (/\) (g . T)
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 monotonic holds
g . A c= (g . E) (/\) (g . T)
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 monotonic holds
g . A c= (g . E) (/\) (g . T)
let g be SetOp of M; :: thesis: for A being Element of Bool M st A = E (/\) T & g is monotonic holds
g . A c= (g . E) (/\) (g . T)
let A be Element of Bool M; :: thesis: ( A = E (/\) T & g is monotonic implies g . A c= (g . E) (/\) (g . T) )
assume A1: A = E (/\) T ; :: thesis: ( not g is monotonic or g . A c= (g . E) (/\) (g . T) )
assume A2: g is monotonic ; :: thesis: g . A c= (g . E) (/\) (g . T)
E (/\) T c= T by PBOOLE:15;
then A3: g . A c= g . T by A1, A2;
E (/\) T c= E by PBOOLE:15;
then g . A c= g . E by A1, A2;
hence g . A c= (g . E) (/\) (g . T) by A3, PBOOLE:17; :: thesis: verum