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;
let i be object ; :: according to PBOOLE:def 2 :: 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 ;
the Sorts of (GenMSAlg A) = MSSubSort A by Th31;
then A1: the Sorts of (GenMSAlg A) . s = meet (SubSort (A,s)) by MSUALG_2:def 14;
the Sorts of (GenOSAlg A) = OSMSubSort A by Th30;
then the Sorts of (GenOSAlg A) . s = meet (OSSubSort (A,s)) by Def11;
hence the Sorts of (GenMSAlg A) . i c= the Sorts of (GenOSAlg A) . i by A1, Th22, SETFAM_1:6; :: thesis: verum