let S be non void Signature; :: thesis: for A being feasible MSAlgebra of S
for B being MSSubAlgebra of A holds B is feasible
let A be feasible MSAlgebra of 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 10;
let o be OperSymbol of S; :: according to MSUALG_6:def 1 :: thesis: ( Args o,B = {} or not Result o,B = {} )
SB is opers_closed by MSUALG_2:def 10;
then SB is_closed_on o by MSUALG_2:def 7;
then A1: rng ((Den o,A) | (((SB # ) * the Arity of S) . o)) c= (SB * the ResultSort of S) . o by MSUALG_2:def 6;
A2: ( Result o,B = (SB * the ResultSort of S) . o & Args o,B = ((SB # ) * the Arity of S) . o ) by MSUALG_1:def 9, MSUALG_1:def 10;
consider a being Element of Args o,B;
assume Args o,B <> {} ; :: thesis: not Result o,B = {}
then A3: ( a in Args o,B & Args o,B c= Args o,A ) by Th38;
then Result o,A <> {} by MSUALG_6:def 1;
then dom (Den o,A) = Args o,A by FUNCT_2:def 1;
then a in dom ((Den o,A) | (Args o,B)) by A3, RELAT_1:86;
then ((Den o,A) | (Args o,B)) . a in rng ((Den o,A) | (Args o,B)) by FUNCT_1:def 5;
hence not Result o,B = {} by A1, A2; :: thesis: verum