let S be non empty non void all-with_const_op ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra of S
for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is non-empty
let U0 be non-empty MSAlgebra of S; :: thesis: for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 /\ the Sorts of U2 is non-empty
let U1, U2 be non-empty MSSubAlgebra of U0; :: thesis: the Sorts of U1 /\ the Sorts of U2 is non-empty
( Constants U0 is V8() MSSubset of U1 & Constants U0 is V8() MSSubset of U2 ) by Th11;
then ( Constants U0 c= the Sorts of U1 & Constants U0 c= the Sorts of U2 ) by PBOOLE:def 23;
then A1: (Constants U0) /\ (Constants U0) c= the Sorts of U1 /\ the Sorts of U2 by PBOOLE:23;

now

let i be set ; :: thesis: ( i in the carrier of S implies not (the Sorts of U1 /\ the Sorts of U2) . i is empty )
assume i in the carrier of S ; :: thesis: not (the Sorts of U1 /\ the Sorts of U2) . i is empty
then reconsider s = i as SortSymbol of S ;
(the Sorts of U1 /\ the Sorts of U2) . s = (the Sorts of U1 . s) /\ (the Sorts of U2 . s) by PBOOLE:def 8;
then A2: (Constants U0) . s c= (the Sorts of U1 . s) /\ (the Sorts of U2 . s) by A1, PBOOLE:def 5;
consider a being set such that
A3: a in (Constants U0) . s by XBOOLE_0:def 1;
thus not (the Sorts of U1 /\ the Sorts of U2) . i is empty by A2, A3, PBOOLE:def 8; :: thesis: verum

end;

hence the Sorts of U1 /\ the Sorts of U2 is non-empty by PBOOLE:def 16; :: thesis: verum