let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of S
for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A
let U0 be MSAlgebra of S; :: thesis: for A being MSSubset of U0 holds (Constants U0) \/ A c= MSSubSort A
let A be MSSubset of U0; :: thesis: (Constants U0) \/ A c= MSSubSort A
let i be set ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S or ((Constants U0) \/ A) . i c= (MSSubSort A) . i )
assume i in the carrier of S ; :: thesis: ((Constants U0) \/ A) . i c= (MSSubSort A) . i
then reconsider s = i as SortSymbol of S ;
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
A2: B in SubSort A and
A3: Z = B . s by Def14;
( Constants U0 c= B & A c= B ) by A2, Th14;
then (Constants U0) \/ A c= B by PBOOLE:16;
hence ((Constants U0) \/ A) . s c= Z by A3, PBOOLE:def 2; :: thesis: verum

end;

(MSSubSort A) . s = meet (SubSort (A,s)) by Def15;
hence ((Constants U0) \/ A) . i c= (MSSubSort A) . i by A1, SETFAM_1:5; :: thesis: verum