let I be set ; :: thesis: for M being ManySortedSet of
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 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 ; :: 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 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 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 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 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 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 holds
( Y in SF iff ( Y in D & A c= Y ) ) by Th31;
thus J .. A = A :: thesis: verum

proof

A in SF by A1, A3;
then meet SF c= A by MSSUBFAM:43;
hence J .. A c= A by A2, A3; :: according to PBOOLE:def 13 :: thesis: A c= J .. A
A4: J .. A = meet SF by A2, A3;
for Z1 being ManySortedSet of st Z1 in SF holds
A c= Z1 by A3;
hence A c= J .. A by A4, MSSUBFAM:45; :: thesis: verum

end;