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 V8() OSSubset of OU1
let OU0 be non-empty OSAlgebra of S; :: thesis: for OU1 being non-empty OSSubAlgebra of OU0 holds OSConstants OU0 is V8() OSSubset of OU1
let OU1 be non-empty OSSubAlgebra of OU0; :: thesis: OSConstants OU0 is V8() OSSubset of OU1
Constants OU0 c= OSConstants OU0 by Th15;
hence OSConstants OU0 is V8() OSSubset of OU1 by Th18, PBOOLE:131; :: thesis: verum