take TrivialTarskiSpace ; :: thesis: ( TrivialTarskiSpace is satisfying_Tarski-model & not TrivialTarskiSpace is empty )
thus ( TrivialTarskiSpace is satisfying_Tarski-model & not TrivialTarskiSpace is empty ) ; :: thesis: verum