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 )
TrivShefferOrthoLattStr is de_Morgan

proof

for x, y being Element of TrivShefferOrthoLattStr holds x "/\" y = ((x ` ) "\/" (y ` )) ` by STRUCT_0:def 10;
hence TrivShefferOrthoLattStr is de_Morgan by ROBBINS1:def 23; :: thesis: verum

end;

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 ) ; :: thesis: verum