take TrivialCTLModel ; :: thesis: TrivialCTLModel is with_basic
thus TrivialCTLModel is with_basic ; :: thesis: verum