let I be set ; :: thesis: for M being ManySortedSet of I

for D being properly-upper-bound MSSubsetFamily of M

for A being Element of bool M

for J being MSSetOp of M st A in D & ( 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

J .. A = A

let M be ManySortedSet of I; :: thesis: for D being properly-upper-bound MSSubsetFamily of M

for A being Element of bool M

for J being MSSetOp of M st A in D & ( 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

J .. A = A

let D be properly-upper-bound MSSubsetFamily of M; :: thesis: for A being Element of bool M

for J being MSSetOp of M st A in D & ( 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

J .. A = A

let A be Element of bool M; :: thesis: for J being MSSetOp of M st A in D & ( 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

J .. A = A

let J be MSSetOp of M; :: thesis: ( A in D & ( 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 J .. A = A )

assume that

A1: A in D 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: J .. A = A

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;

A in SF by A1, A3;

then meet SF c= A by MSSUBFAM:43;

then A4: J .. A c= A by A2, A3;

A5: for Z1 being ManySortedSet of I st Z1 in SF holds

A c= Z1 by A3;

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

then A c= J .. A by A5, MSSUBFAM:45;

hence J .. A = A by A4, PBOOLE:146; :: thesis: verum

for D being properly-upper-bound MSSubsetFamily of M

for A being Element of bool M

for J being MSSetOp of M st A in D & ( 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

J .. A = A

let M be ManySortedSet of I; :: thesis: for D being properly-upper-bound MSSubsetFamily of M

for A being Element of bool M

for J being MSSetOp of M st A in D & ( 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

J .. A = A

let D be properly-upper-bound MSSubsetFamily of M; :: thesis: for A being Element of bool M

for J being MSSetOp of M st A in D & ( 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

J .. A = A

let A be Element of bool M; :: thesis: for J being MSSetOp of M st A in D & ( 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

J .. A = A

let J be MSSetOp of M; :: thesis: ( A in D & ( 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 J .. A = A )

assume that

A1: A in D 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: J .. A = A

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;

A in SF by A1, A3;

then meet SF c= A by MSSUBFAM:43;

then A4: J .. A c= A by A2, A3;

A5: for Z1 being ManySortedSet of I st Z1 in SF holds

A c= Z1 by A3;

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

then A c= J .. A by A5, MSSUBFAM:45;

hence J .. A = A by A4, PBOOLE:146; :: thesis: verum