take TrivLattRelStr ; :: thesis: ( TrivLattRelStr is 1 -element & TrivLattRelStr is reflexive )
thus ( TrivLattRelStr is 1 -element & TrivLattRelStr is reflexive ) ; :: thesis: verum