defpred S₁[ object , object ] means ex Q being Subset-Family of (M . $1) st
( Q = SF . $1 & $2 = Intersect Q );
A1: for i being object st i in I holds
ex j being object st S₁[i,j]

proof

let i be object ; :: thesis: ( i in I implies ex j being object st S₁[i,j] )
assume A2: i in I ; :: thesis: ex j being object st S₁[i,j]
then reconsider Q = SF . i as Subset-Family of (M . i) by Th32;
reconsider a = I --> (Intersect Q) as ManySortedSet of I ;
take a . i ; :: thesis: S₁[i,a . i]
take Q ; :: thesis: ( Q = SF . i & a . i = Intersect Q )
thus ( Q = SF . i & a . i = Intersect Q ) by A2, FUNCOP_1:7; :: thesis: verum

end;

ex X being ManySortedSet of I st
for i being object st i in I holds
S₁[i,X . i] from PBOOLE:sch 3(A1);
hence ex b₁ being ManySortedSet of I st
for i being object st i in I holds
ex Q being Subset-Family of (M . i) st
( Q = SF . i & b₁ . i = Intersect Q ) ; :: thesis: verum