let S be non void Signature; :: thesis: for A being feasible MSAlgebra over S
for B being MSSubAlgebra of A holds B is feasible

let A be feasible MSAlgebra over S; :: thesis: for B being MSSubAlgebra of A holds B is feasible
let B be MSSubAlgebra of A; :: thesis: B is feasible
reconsider SB = the Sorts of B as MSSubset of A by MSUALG_2:def 9;
let o be OperSymbol of S; :: according to MSUALG_6:def 1 :: thesis: ( Args (o,B) = {} or not Result (o,B) = {} )
set a = the Element of Args (o,B);
assume Args (o,B) <> {} ; :: thesis: not Result (o,B) = {}
then A1: the Element of Args (o,B) in Args (o,B) ;
A2: Args (o,B) c= Args (o,A) by Th37;
then Result (o,A) <> {} by ;
then dom (Den (o,A)) = Args (o,A) by FUNCT_2:def 1;
then the Element of Args (o,B) in dom ((Den (o,A)) | (Args (o,B))) by ;
then A3: ( Result (o,B) = (SB * the ResultSort of S) . o & ((Den (o,A)) | (Args (o,B))) . the Element of Args (o,B) in rng ((Den (o,A)) | (Args (o,B))) ) by ;
SB is opers_closed by MSUALG_2:def 9;
then SB is_closed_on o ;
then rng ((Den (o,A)) | (((SB #) * the Arity of S) . o)) c= (SB * the ResultSort of S) . o ;
hence not Result (o,B) = {} by ; :: thesis: verum