let A be X,S -terms MSAlgebra over S; :: thesis: ( A is all_vars_including implies A is non-empty )
assume A1: FreeGen X is ManySortedSubset of the Sorts of A ; :: according to MSAFREE4:def 7 :: thesis: A is non-empty
let x be object ; :: according to MSUALG_1:def 3,PBOOLE:def 13 :: thesis: ( not x in the carrier of S or not the Sorts of A . x is empty )
assume x in the carrier of S ; :: thesis: not the Sorts of A . x is empty
then reconsider x = x as SortSymbol of S ;
(FreeGen X) . x c= the Sorts of A . x by A1, PBOOLE:def 2, PBOOLE:def 18;
hence not the Sorts of A . x is empty ; :: thesis: verum