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