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