let S1 be OrderSortedSign; :: thesis: for OU0 being OSAlgebra of S1
for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )
let OU0 be OSAlgebra of S1; :: thesis: for A being OSSubset of OU0 holds
( OSMSubSort A is opers_closed & A c= OSMSubSort A )
let A be OSSubset of OU0; :: thesis: ( OSMSubSort A is opers_closed & A c= OSMSubSort A )
thus OSMSubSort A is opers_closed :: thesis: A c= OSMSubSort A

proof

let o1 be Element of the carrier' of S1; :: according to MSUALG_2:def 6 :: thesis: OSMSubSort A is_closed_on o1
reconsider o = o1 as OperSymbol of S1 ;
rng ((Den (o,OU0)) | ((((OSMSubSort A) #) * the Arity of S1) . o)) c= ((OSMSubSort A) * the ResultSort of S1) . o by Th28;
hence OSMSubSort A is_closed_on o1 ; :: thesis: verum

end;

( A c= (OSConstants OU0) (\/) A & (OSConstants OU0) (\/) A c= OSMSubSort A ) by Th24, PBOOLE:14;
hence A c= OSMSubSort A by PBOOLE:13; :: thesis: verum