let I be set ; :: thesis: for M being ManySortedSet of
for E, T being Element of Bool M holds E \+\ T in Bool M
let M be ManySortedSet of ; :: thesis: for E, T being Element of Bool M holds E \+\ T in Bool M
let E, T be Element of Bool M; :: thesis: E \+\ T in Bool M
E \+\ T is ManySortedSubset of M

proof

( E c= M & T c= M ) by PBOOLE:def 23;
then ( E \ T c= M & T \ E c= M ) by MBOOLEAN:16;
hence E \+\ T c= M by PBOOLE:99; :: according to PBOOLE:def 23 :: thesis: verum

end;

hence E \+\ T in Bool M by Def1; :: thesis: verum