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

for A being MSSubset of U0 st (Constants U0) (\/) A is V8() holds

MSSubSort A is V8()

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

MSSubSort A is V8()

let A be MSSubset of U0; :: thesis: ( (Constants U0) (\/) A is V8() implies MSSubSort A is V8() )

assume A1: (Constants U0) (\/) A is V8() ; :: thesis: MSSubSort A is V8()

for A being MSSubset of U0 st (Constants U0) (\/) A is V8() holds

MSSubSort A is V8()

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

MSSubSort A is V8()

let A be MSSubset of U0; :: thesis: ( (Constants U0) (\/) 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 (MSSubSort A) . i is empty

hence
MSSubSort A is V8()
; :: thesis: verumnot (MSSubSort A) . i is empty

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

for Z being set st Z in SubSort (A,s) holds

((Constants U0) (\/) A) . s c= Z

ex x being object st x in ((Constants U0) (\/) A) . s by A1, XBOOLE_0:def 1;

hence not (MSSubSort A) . i is empty by A4, Def14; :: thesis: verum

end;assume i in the carrier of S ; :: thesis: not (MSSubSort A) . i is empty

then reconsider s = i as SortSymbol of S ;

for Z being set st Z in SubSort (A,s) holds

((Constants U0) (\/) A) . s c= Z

proof

then A4:
((Constants U0) (\/) A) . s c= meet (SubSort (A,s))
by SETFAM_1:5;
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 Def13;

( Constants U0 c= B & A c= B ) by A2, Th13;

then (Constants U0) (\/) A c= B by PBOOLE:16;

hence ((Constants U0) (\/) A) . s c= Z by A3; :: thesis: verum

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

( Constants U0 c= B & A c= B ) by A2, Th13;

then (Constants U0) (\/) A c= B by PBOOLE:16;

hence ((Constants U0) (\/) A) . s c= Z by A3; :: thesis: verum

ex x being object st x in ((Constants U0) (\/) A) . s by A1, XBOOLE_0:def 1;

hence not (MSSubSort A) . i is empty by A4, Def14; :: thesis: verum