consider B being non empty trivial strict reflexive RelStr ;
take B ; :: thesis: ( B is strict & not B is empty & B is trivial )
thus ( B is strict & not B is empty & B is trivial ) ; :: thesis: verum