let A be MSAlgebra of S; :: thesis: ( A is non-empty implies A is feasible )
assume A is non-empty ; :: thesis: A is feasible
then reconsider B = A as non-empty MSAlgebra of S ;
let o be OperSymbol of S; :: according to MSUALG_6:def 1 :: thesis: ( Args (o,A) <> {} implies Result (o,A) <> {} )
Result (o,B) <> {} ;
hence ( Args (o,A) <> {} implies Result (o,A) <> {} ) ; :: thesis: verum