let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: for x, y being Element of L holds x | ((y | x) | x) = y | x

let x, y be Element of L; :: thesis: x | ((y | x) | x) = y | x

((x | (y | y)) | (x | (y | y))) | (y | x) = (y | x) | x by Th122;

hence x | ((y | x) | x) = y | x by Th108; :: thesis: verum

let x, y be Element of L; :: thesis: x | ((y | x) | x) = y | x

((x | (y | y)) | (x | (y | y))) | (y | x) = (y | x) | x by Th122;

hence x | ((y | x) | x) = y | x by Th108; :: thesis: verum