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