let S1 be OrderSortedSign; :: thesis: for U0 being non-empty OSAlgebra of S1
for U1 being OSSubAlgebra of U0
for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B
let U0 be non-empty OSAlgebra of S1; :: thesis: for U1 being OSSubAlgebra of U0
for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B
let U1 be OSSubAlgebra of U0; :: thesis: for B being OSSubset of U0 st B = the Sorts of U0 holds
(GenOSAlg B) "\/"_os U1 = GenOSAlg B
let B be OSSubset of U0; :: thesis: ( B = the Sorts of U0 implies (GenOSAlg B) "\/"_os U1 = GenOSAlg B )
A1: the Sorts of U1 is MSSubset of U0 by MSUALG_2:def 9;
assume B = the Sorts of U0 ; :: thesis: (GenOSAlg B) "\/"_os U1 = GenOSAlg B
then the Sorts of U1 c= B by A1, PBOOLE:def 18;
then B (\/) the Sorts of U1 = B by PBOOLE:22;
hence (GenOSAlg B) "\/"_os U1 = GenOSAlg B by Th37; :: thesis: verum