let I be set ; :: thesis: for M being ManySortedSet of I
for D being absolutely-multiplicative MSSubsetFamily of M
for A being Element of bool M
for J being MSSetOp of M st J .. A = A & ( 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
A in D
let M be ManySortedSet of I; :: thesis: for D being absolutely-multiplicative MSSubsetFamily of M
for A being Element of bool M
for J being MSSetOp of M st J .. A = A & ( 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
A in D
let D be absolutely-multiplicative MSSubsetFamily of M; :: thesis: for A being Element of bool M
for J being MSSetOp of M st J .. A = A & ( 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
A in D
let A be Element of bool M; :: thesis: for J being MSSetOp of M st J .. A = A & ( 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
A in D
let J be MSSetOp of M; :: thesis: ( J .. A = A & ( 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 A in D )
assume that
A1: J .. A = A and
A2: 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: A in D
defpred S₁[ ManySortedSet of I] means A c= $1;
consider SF being non-empty MSSubsetFamily of M such that
A3: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & A c= Y ) ) by Th31;
A4: ( ( for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & S₁[Y] ) ) ) implies SF c= D ) from CLOSURE1:sch 1();
J .. A = meet SF by A2, A3;
hence A in D by A1, A3, A4, MSSUBFAM:def 5; :: thesis: verum