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

for D being properly-upper-bound MSSubsetFamily of M

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

for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

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

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

for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let D be properly-upper-bound MSSubsetFamily of M; :: thesis: 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

for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let X be Element of bool M; :: thesis: 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

for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let SF be V8() MSSubsetFamily of M; :: thesis: ( ( for Y being ManySortedSet of I holds

( Y in SF iff ( Y in D & X c= Y ) ) ) implies for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z } )

assume A1: for Y being ManySortedSet of I holds

( Y in SF iff ( Y in D & X c= Y ) ) ; :: thesis: for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let i be set ; :: thesis: for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let Di be non empty set ; :: thesis: ( i in I & Di = D . i implies SF . i = { z where z is Element of Di : X . i c= z } )

assume that

A2: i in I and

A3: Di = D . i ; :: thesis: SF . i = { z where z is Element of Di : X . i c= z }

thus SF . i c= { z where z is Element of Di : X . i c= z } :: according to XBOOLE_0:def 10 :: thesis: { z where z is Element of Di : X . i c= z } c= SF . i

assume x in { z where z is Element of Di : X . i c= z } ; :: thesis: x in SF . i

then consider g being Element of Di such that

A11: g = x and

A12: X . i c= g ;

dom (M +* (i .--> g)) = I by A2, PZFMISC1:1;

then reconsider L1 = M +* (i .--> g) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

A13: dom (i .--> g) = {i} ;

i in {i} by TARSKI:def 1;

then A14: L1 . i = (i .--> g) . i by A13, FUNCT_4:13

.= g by FUNCOP_1:72 ;

A15: X c= L1

L1 in D

hence x in SF . i by A2, A11, A14; :: thesis: verum

for D being properly-upper-bound MSSubsetFamily of M

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

for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

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

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

for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let D be properly-upper-bound MSSubsetFamily of M; :: thesis: 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

for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let X be Element of bool M; :: thesis: 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

for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let SF be V8() MSSubsetFamily of M; :: thesis: ( ( for Y being ManySortedSet of I holds

( Y in SF iff ( Y in D & X c= Y ) ) ) implies for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z } )

assume A1: for Y being ManySortedSet of I holds

( Y in SF iff ( Y in D & X c= Y ) ) ; :: thesis: for i being set

for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let i be set ; :: thesis: for Di being non empty set st i in I & Di = D . i holds

SF . i = { z where z is Element of Di : X . i c= z }

let Di be non empty set ; :: thesis: ( i in I & Di = D . i implies SF . i = { z where z is Element of Di : X . i c= z } )

assume that

A2: i in I and

A3: Di = D . i ; :: thesis: SF . i = { z where z is Element of Di : X . i c= z }

thus SF . i c= { z where z is Element of Di : X . i c= z } :: according to XBOOLE_0:def 10 :: thesis: { z where z is Element of Di : X . i c= z } c= SF . i

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { z where z is Element of Di : X . i c= z } or x in SF . i )
consider K being ManySortedSet of I such that

A4: K in SF by PBOOLE:134;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SF . i or x in { z where z is Element of Di : X . i c= z } )

assume A5: x in SF . i ; :: thesis: x in { z where z is Element of Di : X . i c= z }

dom (K +* (i .--> x)) = I by A2, PZFMISC1:1;

then reconsider L = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

A6: dom (i .--> x) = {i} ;

i in {i} by TARSKI:def 1;

then A7: L . i = (i .--> x) . i by A6, FUNCT_4:13

.= x by FUNCOP_1:72 ;

A8: L in SF

then A10: X . i c= L . i by A2;

L in D by A1, A8;

then L . i in D . i by A2;

hence x in { z where z is Element of Di : X . i c= z } by A3, A7, A10; :: thesis: verum

end;A4: K in SF by PBOOLE:134;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SF . i or x in { z where z is Element of Di : X . i c= z } )

assume A5: x in SF . i ; :: thesis: x in { z where z is Element of Di : X . i c= z }

dom (K +* (i .--> x)) = I by A2, PZFMISC1:1;

then reconsider L = K +* (i .--> x) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

A6: dom (i .--> x) = {i} ;

i in {i} by TARSKI:def 1;

then A7: L . i = (i .--> x) . i by A6, FUNCT_4:13

.= x by FUNCOP_1:72 ;

A8: L in SF

proof

then
X c= L
by A1;
let s be object ; :: according to PBOOLE:def 1 :: thesis: ( not s in I or L . s in SF . s )

assume A9: s in I ; :: thesis: L . s in SF . s

end;assume A9: s in I ; :: thesis: L . s in SF . s

then A10: X . i c= L . i by A2;

L in D by A1, A8;

then L . i in D . i by A2;

hence x in { z where z is Element of Di : X . i c= z } by A3, A7, A10; :: thesis: verum

assume x in { z where z is Element of Di : X . i c= z } ; :: thesis: x in SF . i

then consider g being Element of Di such that

A11: g = x and

A12: X . i c= g ;

dom (M +* (i .--> g)) = I by A2, PZFMISC1:1;

then reconsider L1 = M +* (i .--> g) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;

A13: dom (i .--> g) = {i} ;

i in {i} by TARSKI:def 1;

then A14: L1 . i = (i .--> g) . i by A13, FUNCT_4:13

.= g by FUNCOP_1:72 ;

A15: X c= L1

proof

A19:
M in D
by MSSUBFAM:def 6;
let s be object ; :: according to PBOOLE:def 2 :: thesis: ( not s in I or X . s c= L1 . s )

assume A16: s in I ; :: thesis: X . s c= L1 . s

end;assume A16: s in I ; :: thesis: X . s c= L1 . s

L1 in D

proof

then
L1 in SF
by A1, A15;
let s be object ; :: according to PBOOLE:def 1 :: thesis: ( not s in I or L1 . s in D . s )

assume A20: s in I ; :: thesis: L1 . s in D . s

end;assume A20: s in I ; :: thesis: L1 . s in D . s

hence x in SF . i by A2, A11, A14; :: thesis: verum