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