let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: for q, p, x being Element of L holds ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = (x | x) | p
let q, p, x be Element of L; :: thesis: ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = (x | x) | p
((x | x) | p) | ((p | p) | p) = (p | (x | p)) | (p | (x | p)) by SHEFFER1:def 15;
hence ((p | (x | p)) | (p | (x | p))) | (q | (q | q)) = (x | x) | p by Th79; :: thesis: verum