let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
let A be OSSubset of OU0; :: thesis: the Sorts of (GenMSAlg A) c= the Sorts of (GenOSAlg A)
set GM = GenMSAlg A;
set GO = GenOSAlg A;
A1: ( the Sorts of (GenMSAlg A) = MSSubSort A & the Sorts of (GenOSAlg A) = OSMSubSort A ) by Th35, Th36;
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in the carrier of S1 or the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i )
assume i in the carrier of S1 ; :: thesis: the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i
then reconsider s = i as SortSymbol of S1 ;
A2: the Sorts of (GenOSAlg A) . s = meet (OSSubSort A,s) by A1, Def11;
the Sorts of (GenMSAlg A) . s = meet (SubSort A,s) by A1, MSUALG_2:def 15;
hence the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i by A2, Th27, SETFAM_1:7; :: thesis: verum