let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: for y, w being Element of L holds w | y = ((y | y) | (y | y)) | w
let y, w be Element of L; :: thesis: w | y = ((y | y) | (y | y)) | w
(y | y) | (y | y) = y by SHEFFER1:def 13;
hence w | y = ((y | y) | (y | y)) | w by Th81; :: thesis: verum