theorem :: SHEFFER1:30

for L being non empty satisfying_Sheffer_1 ShefferOrthoLattStr
for x being Element of L holds x = (x ") " by Def13;