let S be non empty non void all-with_const_op ManySortedSign ; :: thesis: for U0 being non-empty MSAlgebra over S

for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 (/\) the Sorts of U2 is V8()

let U0 be non-empty MSAlgebra over S; :: thesis: for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 (/\) the Sorts of U2 is V8()

let U1, U2 be non-empty MSSubAlgebra of U0; :: thesis: the Sorts of U1 (/\) the Sorts of U2 is V8()

Constants U0 is V8() MSSubset of U2 by Th10;

then A1: Constants U0 c= the Sorts of U2 by PBOOLE:def 18;

Constants U0 is V8() MSSubset of U1 by Th10;

then Constants U0 c= the Sorts of U1 by PBOOLE:def 18;

then A2: (Constants U0) (/\) (Constants U0) c= the Sorts of U1 (/\) the Sorts of U2 by A1, PBOOLE:21;

for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 (/\) the Sorts of U2 is V8()

let U0 be non-empty MSAlgebra over S; :: thesis: for U1, U2 being non-empty MSSubAlgebra of U0 holds the Sorts of U1 (/\) the Sorts of U2 is V8()

let U1, U2 be non-empty MSSubAlgebra of U0; :: thesis: the Sorts of U1 (/\) the Sorts of U2 is V8()

Constants U0 is V8() MSSubset of U2 by Th10;

then A1: Constants U0 c= the Sorts of U2 by PBOOLE:def 18;

Constants U0 is V8() MSSubset of U1 by Th10;

then Constants U0 c= the Sorts of U1 by PBOOLE:def 18;

then A2: (Constants U0) (/\) (Constants U0) c= the Sorts of U1 (/\) the Sorts of U2 by A1, PBOOLE:21;

now :: thesis: for i being object st i in the carrier of S holds

not ( the Sorts of U1 (/\) the Sorts of U2) . i is empty

hence
the Sorts of U1 (/\) the Sorts of U2 is V8()
; :: thesis: verumnot ( the Sorts of U1 (/\) the Sorts of U2) . i is empty

let i be object ; :: 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 5;

then A3: (Constants U0) . s c= ( the Sorts of U1 . s) /\ ( the Sorts of U2 . s) by A2;

ex a being object st a in (Constants U0) . s by XBOOLE_0:def 1;

hence not ( the Sorts of U1 (/\) the Sorts of U2) . i is empty by A3, PBOOLE:def 5; :: thesis: verum

end;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 5;

then A3: (Constants U0) . s c= ( the Sorts of U1 . s) /\ ( the Sorts of U2 . s) by A2;

ex a being object st a in (Constants U0) . s by XBOOLE_0:def 1;

hence not ( the Sorts of U1 (/\) the Sorts of U2) . i is empty by A3, PBOOLE:def 5; :: thesis: verum