take TrivShefferOrthoLattStr ; :: thesis: ( TrivShefferOrthoLattStr is satisfying_Sh_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 )
thus ( TrivShefferOrthoLattStr is satisfying_Sh_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_1 & TrivShefferOrthoLattStr is satisfying_Sheffer_2 & TrivShefferOrthoLattStr is satisfying_Sheffer_3 ) ; :: thesis: verum