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
proof
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 ;
then reconsider L = K +* (i .--> x) as ManySortedSet of I by ;
A6: dom (i .--> x) = {i} ;
i in {i} by TARSKI:def 1;
then A7: L . i = (i .--> x) . i by
.= x by FUNCOP_1:72 ;
A8: L in SF
proof
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
per cases ( s = i or s <> i ) ;
suppose s = i ; :: thesis: L . s in SF . s
hence L . s in SF . s by A5, A7; :: thesis: verum
end;
suppose s <> i ; :: thesis: L . s in SF . s
then not s in dom (i .--> x) by TARSKI:def 1;
then L . s = K . s by FUNCT_4:11;
hence L . s in SF . s by A4, A9; :: thesis: verum
end;
end;
end;
then X c= L by A1;
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;
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 )
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 ;
then reconsider L1 = M +* (i .--> g) as ManySortedSet of I by ;
A13: dom (i .--> g) = {i} ;
i in {i} by TARSKI:def 1;
then A14: L1 . i = (i .--> g) . i by
.= g by FUNCOP_1:72 ;
A15: X c= L1
proof
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
per cases ( s = i or s <> i ) ;
suppose s = i ; :: thesis: X . s c= L1 . s
hence X . s c= L1 . s by ; :: thesis: verum
end;
end;
end;
A19: M in D by MSSUBFAM:def 6;
L1 in D
proof
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
per cases ( s = i or s <> i ) ;
suppose s = i ; :: thesis: L1 . s in D . s
hence L1 . s in D . s by ; :: thesis: verum
end;
suppose s <> i ; :: thesis: L1 . s in D . s
then not s in dom (i .--> g) by TARSKI:def 1;
then L1 . s = M . s by FUNCT_4:11;
hence L1 . s in D . s by ; :: thesis: verum
end;
end;
end;
then L1 in SF by ;
hence x in SF . i by A2, A11, A14; :: thesis: verum