set B = the 1 -element strict reflexive RelStr ;
take the 1 -element strict reflexive RelStr ; :: thesis: ( the 1 -element strict reflexive RelStr is strict & the 1 -element strict reflexive RelStr is 1 -element )
thus ( the 1 -element strict reflexive RelStr is strict & the 1 -element strict reflexive RelStr is 1 -element ) ; :: thesis: verum