let S be non empty non void ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S
for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
let U0 be non-empty MSAlgebra of S; :: thesis: for A, B being strict non-empty finitely-generated MSSubAlgebra of U0 ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
let A, B be strict non-empty finitely-generated MSSubAlgebra of U0; :: thesis: ex M being strict non-empty finitely-generated MSSubAlgebra of U0 st
( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
defpred S₁[ set , set ] means ( ( $1 = 0 implies $2 = A ) & ( $1 = 1 implies $2 = B ) );
A1: for i being set st i in {0 ,1} holds
ex j being set st S₁[i,j]

proof

let i be set ; :: thesis: ( i in {0 ,1} implies ex j being set st S₁[i,j] )
assume A2: i in {0 ,1} ; :: thesis: ex j being set st S₁[i,j]

per cases ( i = 0 or i = 1 ) by A2, TARSKI:def 2;

suppose A3: i = 0 ; :: thesis: ex j being set st S₁[i,j]

take A ; :: thesis: S₁[i,A]
thus S₁[i,A] by A3; :: thesis: verum

end;

suppose A4: i = 1 ; :: thesis: ex j being set st S₁[i,j]

take B ; :: thesis: S₁[i,B]
thus S₁[i,B] by A4; :: thesis: verum

end;

end;

end;

consider F being ManySortedSet of {0 ,1} such that
A5: for i being set st i in {0 ,1} holds
S₁[i,F . i] from PBOOLE:sch 3(A1);
F is MSAlgebra-Family of {0 ,1},S

proof

let i be set ; :: according to PRALG_2:def 12 :: thesis: ( not i in {0 ,1} or F . i is MSAlgebra of S )
assume A6: i in {0 ,1} ; :: thesis: F . i is MSAlgebra of S
then A7: ( i = 1 implies F . i = B ) by A5;
( i = 0 implies F . i = A ) by A5, A6;
hence F . i is MSAlgebra of S by A6, A7, TARSKI:def 2; :: thesis: verum

end;

then reconsider F = F as MSAlgebra-Family of {0 ,1},S ;
for i being Element of {0 ,1} ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i

proof

let i be Element of {0 ,1}; :: thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i

per cases ( i = 0 or i = 1 ) by TARSKI:def 2;

suppose A8: i = 0 ; :: thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i

take A ; :: thesis: A = F . i
thus A = F . i by A5, A8; :: thesis: verum

end;

suppose A9: i = 1 ; :: thesis: ex C being strict non-empty finitely-generated MSSubAlgebra of U0 st C = F . i

take B ; :: thesis: B = F . i
thus B = F . i by A5, A9; :: thesis: verum

end;

end;

end;

then consider M being strict non-empty finitely-generated MSSubAlgebra of U0 such that
A10: for i being Element of {0 ,1} holds F . i is MSSubAlgebra of M by Th27;
take M ; :: thesis: ( A is MSSubAlgebra of M & B is MSSubAlgebra of M )
A11: 0 in {0 ,1} by TARSKI:def 2;
then F . 0 = A by A5;
hence A is MSSubAlgebra of M by A10, A11; :: thesis: B is MSSubAlgebra of M
A12: 1 in {0 ,1} by TARSKI:def 2;
then F . 1 = B by A5;
hence B is MSSubAlgebra of M by A10, A12; :: thesis: verum