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

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