let S be all-with_const_op OrderSortedSign; :: thesis: for OU0 being non-empty OSAlgebra of S
for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is non-empty OSSubset of OU1
let OU0 be non-empty OSAlgebra of S; :: thesis: for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is non-empty OSSubset of OU1
let OU1 be non-empty OSSubAlgebra of OU0; :: thesis: OSConstants OU0 is non-empty OSSubset of OU1
Constants OU0 c= OSConstants OU0 by Th10;
hence OSConstants OU0 is non-empty OSSubset of OU1 by Th13, PBOOLE:131; :: thesis: verum