take TrivCLRelStr ; :: thesis: ( TrivCLRelStr is with_infima & TrivCLRelStr is with_suprema & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is naturally_inf-generated & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is OrderInvolutive & TrivCLRelStr is Pure & TrivCLRelStr is PartialOrdered )
thus ( TrivCLRelStr is with_infima & TrivCLRelStr is with_suprema & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is naturally_inf-generated & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is OrderInvolutive & TrivCLRelStr is Pure & TrivCLRelStr is PartialOrdered ) ; :: thesis: verum