let I be set ; :: thesis: for A, M being ManySortedSet of
for E being Element of Bool M holds E \ A in Bool M
let A, M be ManySortedSet of ; :: 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 \ A is ManySortedSubset of M

proof

E c= M by PBOOLE:def 23;
hence E \ A c= M by MBOOLEAN:16; :: according to PBOOLE:def 23 :: thesis: verum

end;

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