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