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 ( ( i = 0 implies F . i = A ) & ( i = 1 implies F . i = B ) ) by A5;
hence F . i is non-empty MSAlgebra of S by A6, 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 A7: 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, A7; :: thesis: verum

end;

suppose A8: 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, A8; :: thesis: verum

end;

end;

end;

then consider M being strict non-empty finitely-generated MSSubAlgebra of U0 such that
A9: 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 )
A10: 0 in {0 ,1} by TARSKI:def 2;
then F . 0 = A by A5;
hence A is MSSubAlgebra of M by A9, A10; :: thesis: B is MSSubAlgebra of M
A11: 1 in {0 ,1} by TARSKI:def 2;
then F . 1 = B by A5;
hence B is MSSubAlgebra of M by A9, A11; :: thesis: verum