let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra over S
for A being MSSubset of U0 st () (\/) A is V8() holds
MSSubSort A is V8()

let U0 be MSAlgebra over S; :: thesis: for A being MSSubset of U0 st () (\/) A is V8() holds
MSSubSort A is V8()

let A be MSSubset of U0; :: thesis: ( () (\/) A is V8() implies MSSubSort A is V8() )
assume A1: (Constants U0) (\/) A is V8() ; :: thesis: MSSubSort A is V8()
now :: thesis: for i being object st i in the carrier of S holds
not () . i is empty
let i be object ; :: thesis: ( i in the carrier of S implies not () . i is empty )
assume i in the carrier of S ; :: thesis: not () . i is empty
then reconsider s = i as SortSymbol of S ;
for Z being set st Z in SubSort (A,s) holds
(() (\/) A) . s c= Z
proof
let Z be set ; :: thesis: ( Z in SubSort (A,s) implies (() (\/) A) . s c= Z )
assume Z in SubSort (A,s) ; :: thesis: (() (\/) A) . s c= Z
then consider B being MSSubset of U0 such that
A2: B in SubSort A and
A3: Z = B . s by Def13;
( Constants U0 c= B & A c= B ) by ;
then (Constants U0) (\/) A c= B by PBOOLE:16;
hence ((Constants U0) (\/) A) . s c= Z by A3; :: thesis: verum
end;
then A4: ((Constants U0) (\/) A) . s c= meet (SubSort (A,s)) by SETFAM_1:5;
ex x being object st x in (() (\/) A) . s by ;
hence not (MSSubSort A) . i is empty by ; :: thesis: verum
end;
hence MSSubSort A is V8() ; :: thesis: verum