let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds (OSConstants OU0) (\/) A c= OSMSubSort A
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds (OSConstants OU0) (\/) A c= OSMSubSort A
let A be OSSubset of OU0; :: thesis: (OSConstants OU0) (\/) A c= OSMSubSort A
let i be object ; :: according to PBOOLE:def 2 :: thesis: ( not i in the carrier of S1 or ((OSConstants OU0) (\/) A) . i c= (OSMSubSort A) . i )
assume i in the carrier of S1 ; :: thesis: ((OSConstants OU0) (\/) A) . i c= (OSMSubSort A) . i
then reconsider s = i as SortSymbol of S1 ;
A1: for Z being set st Z in OSSubSort (A,s) holds
((OSConstants OU0) (\/) A) . s c= Z

proof

let Z be set ; :: thesis: ( Z in OSSubSort (A,s) implies ((OSConstants OU0) (\/) A) . s c= Z )
assume Z in OSSubSort (A,s) ; :: thesis: ((OSConstants OU0) (\/) A) . s c= Z
then consider B being OSSubset of OU0 such that
A2: B in OSSubSort A and
A3: Z = B . s by Def10;
( OSConstants OU0 c= B & A c= B ) by A2, Th19;
then (OSConstants OU0) (\/) A c= B by PBOOLE:16;
hence ((OSConstants OU0) (\/) A) . s c= Z by A3; :: thesis: verum

end;

(OSMSubSort A) . s = meet (OSSubSort (A,s)) by Def11;
hence ((OSConstants OU0) (\/) A) . i c= (OSMSubSort A) . i by A1, SETFAM_1:5; :: thesis: verum