let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
let U0 be non-empty OSAlgebra of S1; :: thesis: for U1 being OSSubAlgebra of U0 holds (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
let U1 be OSSubAlgebra of U0; :: thesis: (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0)
set C = OSConstants U0;
set G = GenOSAlg (OSConstants U0);
OSConstants U0 is OSSubset of U1 by Th13;
then GenOSAlg (OSConstants U0) is strict OSSubAlgebra of U1 by Def12;
then the Sorts of (GenOSAlg (OSConstants U0)) is MSSubset of U1 by MSUALG_2:def 9;
then ( the Sorts of ((GenOSAlg (OSConstants U0)) /\ U1) = the Sorts of (GenOSAlg (OSConstants U0)) (/\) the Sorts of U1 & the Sorts of (GenOSAlg (OSConstants U0)) c= the Sorts of U1 ) by MSUALG_2:def 16, PBOOLE:def 18;
then the Sorts of ((GenOSAlg (OSConstants U0)) /\ U1) = the Sorts of (GenOSAlg (OSConstants U0)) by PBOOLE:23;
hence (GenOSAlg (OSConstants U0)) /\ U1 = GenOSAlg (OSConstants U0) by MSUALG_2:9; :: thesis: verum