let I be set ; :: thesis: for M being ManySortedSet of I
for E, T being Element of Bool M holds E \+\ T in Bool M
let M be ManySortedSet of I; :: 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
T c= M by PBOOLE:def 23;
then A1: T \ E c= M by MBOOLEAN:16;
E c= M by PBOOLE:def 23;
then E \ T c= M by MBOOLEAN:16;
then E \+\ T c= M by A1, PBOOLE:99;
then E \+\ T is ManySortedSubset of M by PBOOLE:def 23;
hence E \+\ T in Bool M by Def1; :: thesis: verum