let I be set ; :: thesis: for M being ManySortedSet of
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 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 is reflexive & J is monotonic )
let M be ManySortedSet of ; :: 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 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 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 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 is reflexive & J is monotonic )
let J be MSSetOp of M; :: thesis: ( ( 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 is reflexive & J is monotonic ) )
assume A1: 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 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 2 :: thesis: X c= J .. X
consider SF being V8() MSSubsetFamily of M such that
A2: for Y being ManySortedSet of holds
( Y in SF iff ( Y in D & X c= Y ) ) by Th31;
A3: J .. X = meet SF by A1, A2;
for Z1 being ManySortedSet of st Z1 in SF holds
X c= Z1 by A2;
hence X c= J .. X by A3, MSSUBFAM:45; :: thesis: verum

end;

thus J is monotonic :: thesis: verum

proof

let x, y be Element of bool M; :: according to CLOSURE1:def 3 :: thesis: ( x c= y implies J .. x c= J .. y )
assume A4: x c= y ; :: thesis: J .. x c= J .. y
consider SFx being V8() MSSubsetFamily of M such that
A5: for Y being ManySortedSet of holds
( Y in SFx iff ( Y in D & x c= Y ) ) by Th31;
A6: J .. x = meet SFx by A1, A5;
consider SFy being V8() MSSubsetFamily of M such that
A7: for Y being ManySortedSet of holds
( Y in SFy iff ( Y in D & y c= Y ) ) by Th31;
SFy c= SFx

proof

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

end;

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

end;