let L be non empty satisfying_Sheffer_1 satisfying_Sheffer_2 satisfying_Sheffer_3 ShefferStr ; :: thesis: for w, q, p being Element of L holds (p | q) | w = w | (q | p)
let w, q, p be Element of L; :: thesis: (p | q) | w = w | (q | p)
w | (p | q) = (p | q) | w by Th83;
hence (p | q) | w = w | (q | p) by Th152; :: thesis: verum