take TrivShefferOrthoLattStr ; :: thesis: ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is de_Morgan & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 & TrivShefferOrthoLattStr is satisfying_Sh_1 )
for x, y being Element of TrivShefferOrthoLattStr holds x "/\" y = ((x `) "\/" (y `)) ` by STRUCT_0:def 10;
hence ( TrivShefferOrthoLattStr is properly_defined & TrivShefferOrthoLattStr is Boolean & TrivShefferOrthoLattStr is well-complemented & TrivShefferOrthoLattStr is Lattice-like & TrivShefferOrthoLattStr is de_Morgan & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 & TrivShefferOrthoLattStr is satisfying_Sh_1 ) by ROBBINS1:def 23; :: thesis: verum