take TrivShefferOrthoLattStr ; :: thesis: ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 )
thus ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 ) ; :: thesis: verum