let I be set ; :: thesis: for M being ManySortedSet of I
for D being properly-upper-bound MSSubsetFamily of M
for J being MSSetOp of M st ( 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 is reflexive & J is monotonic )
let M be ManySortedSet of I; :: thesis: for D being properly-upper-bound MSSubsetFamily of M
for J being MSSetOp of M st ( 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 is reflexive & J is monotonic )
let D be properly-upper-bound MSSubsetFamily of M; :: thesis: for J being MSSetOp of M st ( 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 is reflexive & J is monotonic )
let J be MSSetOp of M; :: thesis: ( ( 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 is reflexive & J is monotonic ) )
assume A1: 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 is reflexive & J is monotonic )
thus J is reflexive :: thesis: J is monotonic

proof

let X be Element of bool M; :: according to CLOSURE1:def 1 :: thesis: X c= J .. X
consider SF being non-empty MSSubsetFamily of M such that
A2: for Y being ManySortedSet of I holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
( J .. X = meet SF & ( for Z1 being ManySortedSet of I st Z1 in SF holds
X c= Z1 ) ) by A1, A2;
hence X c= J .. X by MSSUBFAM:45; :: thesis: verum

end;

thus J is monotonic :: thesis: verum

proof

let x, y be Element of bool M; :: according to CLOSURE1:def 2 :: thesis: ( x c= y implies J .. x c= J .. y )
assume A3: x c= y ; :: thesis: J .. x c= J .. y
consider SFx being non-empty MSSubsetFamily of M such that
A4: for Y being ManySortedSet of I holds
( Y in SFx iff ( Y in D & x c= Y ) ) by Th31;
consider SFy being non-empty MSSubsetFamily of M such that
A5: for Y being ManySortedSet of I holds
( Y in SFy iff ( Y in D & y c= Y ) ) by Th31;
SFy c= SFx

proof

let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in I or SFy . i c= SFx . i )
assume A6: i in I ; :: thesis: SFy . i c= SFx . i
then consider Fi being non empty set such that
A7: Fi = D . i ;
A8: x . i c= y . i by A3, A6;
( SFx . i = { t where t is Element of Fi : x . i c= t } & SFy . i = { z where z is Element of Fi : y . i c= z } ) by A4, A5, A6, A7, Th32;
hence SFy . i c= SFx . i by A8, Th1; :: thesis: verum

end;

then A9: meet SFx c= meet SFy by MSSUBFAM:46;
J .. x = meet SFx by A1, A4;
hence J .. x c= J .. y by A1, A5, A9; :: thesis: verum

end;