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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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_{1}[ ManySortedSet of I] means A c= $1;

consider SF being V8() 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_{1}[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

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 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 V8() 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 V8() 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 V8() 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 V8() 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 V8() 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

consider SF being V8() 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

J .. A = meet SF by A2, A3;

hence A in D by A1, A3, A4, MSSUBFAM:def 5; :: thesis: verum