take TrivCLRelStr ; :: thesis: ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is well-complemented )
thus ( TrivCLRelStr is involutive & TrivCLRelStr is with_Top & TrivCLRelStr is de_Morgan & TrivCLRelStr is Lattice-like & TrivCLRelStr is naturally_sup-generated & TrivCLRelStr is well-complemented ) ; :: thesis: verum