defpred S_{1}[ object , object ] means $2 = union { (f . $1) where f is Element of Bool M : f in A } ;

A1: for x being object st x in I holds

ex y being object st S_{1}[x,y]
;

consider IT being Function such that

A2: dom IT = I and

A3: for x being object st x in I holds

S_{1}[x,IT . x]
from CLASSES1:sch 1(A1);

reconsider IT = IT as ManySortedSet of I by A2, PARTFUN1:def 2, RELAT_1:def 18;

for i being object st i in I holds

IT . i c= M . i

then reconsider IT = IT as ManySortedSubset of M by PBOOLE:def 18;

take IT ; :: thesis: for i being set st i in I holds

IT . i = union { (f . i) where f is Element of Bool M : f in A }

thus for i being set st i in I holds

IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3; :: thesis: verum

A1: for x being object st x in I holds

ex y being object st S

consider IT being Function such that

A2: dom IT = I and

A3: for x being object st x in I holds

S

reconsider IT = IT as ManySortedSet of I by A2, PARTFUN1:def 2, RELAT_1:def 18;

for i being object st i in I holds

IT . i c= M . i

proof

then
IT c= M
;
let i be object ; :: thesis: ( i in I implies IT . i c= M . i )

assume A4: i in I ; :: thesis: IT . i c= M . i

for x being object st x in IT . i holds

x in M . i

end;assume A4: i in I ; :: thesis: IT . i c= M . i

for x being object st x in IT . i holds

x in M . i

proof

hence
IT . i c= M . i
; :: thesis: verum
let x be object ; :: thesis: ( x in IT . i implies x in M . i )

assume A5: x in IT . i ; :: thesis: x in M . i

IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3, A4;

then consider Y being set such that

A6: x in Y and

A7: Y in { (f . i) where f is Element of Bool M : f in A } by A5, TARSKI:def 4;

consider ff being Element of Bool M such that

A8: ff . i = Y and

ff in A by A7;

reconsider ff = ff as ManySortedSubset of M ;

ff c= M by PBOOLE:def 18;

then ff . i c= M . i by A4;

hence x in M . i by A6, A8; :: thesis: verum

end;assume A5: x in IT . i ; :: thesis: x in M . i

IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3, A4;

then consider Y being set such that

A6: x in Y and

A7: Y in { (f . i) where f is Element of Bool M : f in A } by A5, TARSKI:def 4;

consider ff being Element of Bool M such that

A8: ff . i = Y and

ff in A by A7;

reconsider ff = ff as ManySortedSubset of M ;

ff c= M by PBOOLE:def 18;

then ff . i c= M . i by A4;

hence x in M . i by A6, A8; :: thesis: verum

then reconsider IT = IT as ManySortedSubset of M by PBOOLE:def 18;

take IT ; :: thesis: for i being set st i in I holds

IT . i = union { (f . i) where f is Element of Bool M : f in A }

thus for i being set st i in I holds

IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3; :: thesis: verum