let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S
for A being MSSubset of U0 st (Constants U0) \/ A is non-empty holds
MSSubSort A is non-empty
let U0 be MSAlgebra of S; :: thesis: for A being MSSubset of U0 st (Constants U0) \/ A is non-empty holds
MSSubSort A is non-empty
let A be MSSubset of U0; :: thesis: ( (Constants U0) \/ A is non-empty implies MSSubSort A is non-empty )
assume A1: (Constants U0) \/ A is non-empty ; :: thesis: MSSubSort A is non-empty

now

let i be set ; :: thesis: ( i in the carrier of S implies not (MSSubSort A) . i is empty )
assume i in the carrier of S ; :: thesis: not (MSSubSort A) . i is empty
then reconsider s = i as SortSymbol of S ;
A2: not ((Constants U0) \/ A) . s is empty by A1;
for Z being set st Z in SubSort A,s holds
((Constants U0) \/ A) . s c= Z

proof

let Z be set ; :: thesis: ( Z in SubSort A,s implies ((Constants U0) \/ A) . s c= Z )
assume Z in SubSort A,s ; :: thesis: ((Constants U0) \/ A) . s c= Z
then consider B being MSSubset of U0 such that
A3: ( B in SubSort A & Z = B . s ) by Def14;
( Constants U0 c= B & A c= B ) by A3, Th14;
then (Constants U0) \/ A c= B by PBOOLE:18;
hence ((Constants U0) \/ A) . s c= Z by A3, PBOOLE:def 5; :: thesis: verum

end;

then A4: ((Constants U0) \/ A) . s c= meet (SubSort A,s) by SETFAM_1:6;
consider x being set such that
A5: x in ((Constants U0) \/ A) . s by A2, XBOOLE_0:def 1;
thus not (MSSubSort A) . i is empty by A4, A5, Def15; :: thesis: verum

end;

hence MSSubSort A is non-empty by PBOOLE:def 16; :: thesis: verum