take TrivLattRelStr ; :: thesis: ( TrivLattRelStr is trivial & not TrivLattRelStr is empty & TrivLattRelStr is reflexive )
thus ( TrivLattRelStr is trivial & not TrivLattRelStr is empty & TrivLattRelStr is reflexive ) ; :: thesis: verum