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