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