take TrivLattRelStr ; :: thesis: ( TrivLattRelStr is antisymmetric & TrivLattRelStr is reflexive & TrivLattRelStr is transitive & TrivLattRelStr is with_suprema & TrivLattRelStr is with_infima )
thus ( TrivLattRelStr is antisymmetric & TrivLattRelStr is reflexive & TrivLattRelStr is transitive & TrivLattRelStr is with_suprema & TrivLattRelStr is with_infima ) ; :: thesis: verum