thus not the BasicAssign of TrivialLTLModel is empty ; :: according to MODELC_2:def 30 :: thesis: ( TrivialLTLModel is strict & not TrivialLTLModel is empty )
thus ( TrivialLTLModel is strict & not TrivialLTLModel is empty ) ; :: thesis: verum