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 18;
then E (\) A c= M by MBOOLEAN:15;
then E (\) A is ManySortedSubset of M by PBOOLE:def 18;
hence E (\) A in Bool M by Def1; :: thesis: verum