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