set A = the non-empty trivial MSAlgebra over S;
take the non-empty trivial MSAlgebra over S ; :: thesis: ( the non-empty trivial MSAlgebra over S is T -satisfying & the non-empty trivial MSAlgebra over S is non-empty & the non-empty trivial MSAlgebra over S is trivial )
thus the non-empty trivial MSAlgebra over S |= T by Th32; :: according to MSAFREE4:def 11 :: thesis: ( the non-empty trivial MSAlgebra over S is non-empty & the non-empty trivial MSAlgebra over S is trivial )
thus ( the non-empty trivial MSAlgebra over S is non-empty & the non-empty trivial MSAlgebra over S is trivial ) ; :: thesis: verum