let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: for y, w, z, v, x being Element of L holds (w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z)) = z | (x | v)
let y, w, z, v, x be Element of L; :: thesis: (w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z)) = z | (x | v)
(z | (x | v)) | (z | (x | v)) = ((x | (y | (y | y))) | z) | ((v | v) | z) by Th73;
hence (w | (z | (x | v))) | (((x | (y | (y | y))) | z) | ((v | v) | z)) = z | (x | v) by Th133; :: thesis: verum