take TrivialLTLModel ; :: thesis: not TrivialLTLModel is empty
thus not TrivialLTLModel is empty ; :: thesis: verum