take TrivLattRelStr ; :: thesis: ( TrivLattRelStr is with_infima & TrivLattRelStr is with_suprema & TrivLattRelStr is naturally_sup-generated & TrivLattRelStr is naturally_inf-generated & TrivLattRelStr is Lattice-like )
thus ( TrivLattRelStr is with_infima & TrivLattRelStr is with_suprema & TrivLattRelStr is naturally_sup-generated & TrivLattRelStr is naturally_inf-generated & TrivLattRelStr is Lattice-like ) ; :: thesis: verum