let I be set ; :: thesis: for M being ManySortedSet of I
for D being absolutely-multiplicative MSSubsetFamily of M
for J being MSSetOp of M st ( for X being Element of bool M
for SF being non-empty MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent
let M be ManySortedSet of I; :: thesis: for D being absolutely-multiplicative MSSubsetFamily of M
for J being MSSetOp of M st ( for X being Element of bool M
for SF being non-empty MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent
let D be absolutely-multiplicative MSSubsetFamily of M; :: thesis: for J being MSSetOp of M st ( for X being Element of bool M
for SF being non-empty MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) holds
J is idempotent
let J be MSSetOp of M; :: thesis: ( ( for X being Element of bool M
for SF being non-empty MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ) implies J is idempotent )
assume A1: for X being Element of bool M
for SF being non-empty MSSubsetFamily of M st ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) ) holds
J .. X = meet SF ; :: thesis: J is idempotent
let X be Element of bool M; :: according to CLOSURE1:def 3 :: thesis: J .. X = J .. (J .. X)
defpred S1[ ManySortedSet of I] means X c= $1;
consider SF being non-empty MSSubsetFamily of M such that
A2: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
( ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & S1[Y] ) ) ) implies SF c= D ) from CLOSURE1:sch 1();
 then A3: meet SF in D by A2, MSSUBFAM:def 5;
D c= bool M by PBOOLE:def 18;
then A4: meet SF is Element of bool M by A3, MSSUBFAM:11, PBOOLE:9;
thus J .. X = meet SF by A1, A2
.= J .. (meet SF) by A1, A3, A4, Th34
.= J .. (J .. X) by A1, A2 ; :: thesis: verum