let I be set ; :: thesis: for A, M being ManySortedSet of I
for E being Element of Bool M holds E \ A in Bool M
let A, M be ManySortedSet of I; :: thesis: for E being Element of Bool M holds E \ A in Bool M
let E be Element of Bool M; :: thesis: E \ A in Bool M
E c= M by PBOOLE:def 23;
then E \ A c= M by MBOOLEAN:16;
then E \ A is ManySortedSubset of M by PBOOLE:def 23;
hence E \ A in Bool M by Def1; :: thesis: verum