thus not the BasicAssign of TrivialCTLModel is empty ; :: according to MODELC_1:def 29 :: thesis: ( TrivialCTLModel is strict & not TrivialCTLModel is empty )
thus ( TrivialCTLModel is strict & not TrivialCTLModel is empty ) ; :: thesis: verum