set B = the non empty trivial strict reflexive RelStr ;
take the non empty trivial strict reflexive RelStr ; :: thesis: ( the non empty trivial strict reflexive RelStr is strict & not the non empty trivial strict reflexive RelStr is empty & the non empty trivial strict reflexive RelStr is trivial )
thus ( the non empty trivial strict reflexive RelStr is strict & not the non empty trivial strict reflexive RelStr is empty & the non empty trivial strict reflexive RelStr is trivial ) ; :: thesis: verum